This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fveqdmss

Description: If the empty set is not contained in the range of a function, and the function values of another class (not necessarily a function) are equal to the function values of the function for all elements of the domain of the function, then the domain of the function is contained in the domain of the class. (Contributed by AV, 28-Jan-2020)

Ref Expression
Hypothesis fveqdmss.1 
|- D = dom B
Assertion fveqdmss 
|- ( ( Fun B /\ (/) e/ ran B /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> D C_ dom A )

Proof

Step Hyp Ref Expression
1 fveqdmss.1 
 |-  D = dom B
2 fveq2 
 |-  ( x = a -> ( A ` x ) = ( A ` a ) )
3 fveq2 
 |-  ( x = a -> ( B ` x ) = ( B ` a ) )
4 2 3 eqeq12d 
 |-  ( x = a -> ( ( A ` x ) = ( B ` x ) <-> ( A ` a ) = ( B ` a ) ) )
5 4 rspcva 
 |-  ( ( a e. D /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> ( A ` a ) = ( B ` a ) )
6 nelrnfvne 
 |-  ( ( Fun B /\ a e. dom B /\ (/) e/ ran B ) -> ( B ` a ) =/= (/) )
7 n0 
 |-  ( ( B ` a ) =/= (/) <-> E. b b e. ( B ` a ) )
8 eleq2 
 |-  ( ( B ` a ) = ( A ` a ) -> ( b e. ( B ` a ) <-> b e. ( A ` a ) ) )
9 8 eqcoms 
 |-  ( ( A ` a ) = ( B ` a ) -> ( b e. ( B ` a ) <-> b e. ( A ` a ) ) )
10 elfvdm 
 |-  ( b e. ( A ` a ) -> a e. dom A )
11 9 10 biimtrdi 
 |-  ( ( A ` a ) = ( B ` a ) -> ( b e. ( B ` a ) -> a e. dom A ) )
12 11 com12 
 |-  ( b e. ( B ` a ) -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) )
13 12 exlimiv 
 |-  ( E. b b e. ( B ` a ) -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) )
14 7 13 sylbi 
 |-  ( ( B ` a ) =/= (/) -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) )
15 6 14 syl 
 |-  ( ( Fun B /\ a e. dom B /\ (/) e/ ran B ) -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) )
16 15 3exp 
 |-  ( Fun B -> ( a e. dom B -> ( (/) e/ ran B -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) ) ) )
17 16 com12 
 |-  ( a e. dom B -> ( Fun B -> ( (/) e/ ran B -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) ) ) )
18 17 1 eleq2s 
 |-  ( a e. D -> ( Fun B -> ( (/) e/ ran B -> ( ( A ` a ) = ( B ` a ) -> a e. dom A ) ) ) )
19 18 com24 
 |-  ( a e. D -> ( ( A ` a ) = ( B ` a ) -> ( (/) e/ ran B -> ( Fun B -> a e. dom A ) ) ) )
20 19 adantr 
 |-  ( ( a e. D /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> ( ( A ` a ) = ( B ` a ) -> ( (/) e/ ran B -> ( Fun B -> a e. dom A ) ) ) )
21 5 20 mpd 
 |-  ( ( a e. D /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> ( (/) e/ ran B -> ( Fun B -> a e. dom A ) ) )
22 21 ex 
 |-  ( a e. D -> ( A. x e. D ( A ` x ) = ( B ` x ) -> ( (/) e/ ran B -> ( Fun B -> a e. dom A ) ) ) )
23 22 com23 
 |-  ( a e. D -> ( (/) e/ ran B -> ( A. x e. D ( A ` x ) = ( B ` x ) -> ( Fun B -> a e. dom A ) ) ) )
24 23 com14 
 |-  ( Fun B -> ( (/) e/ ran B -> ( A. x e. D ( A ` x ) = ( B ` x ) -> ( a e. D -> a e. dom A ) ) ) )
25 24 3imp 
 |-  ( ( Fun B /\ (/) e/ ran B /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> ( a e. D -> a e. dom A ) )
26 25 ssrdv 
 |-  ( ( Fun B /\ (/) e/ ran B /\ A. x e. D ( A ` x ) = ( B ` x ) ) -> D C_ dom A )