Metamath Proof Explorer

Theorem mpteqb

Description: Bidirectional equality theorem for a mapping abstraction. Equivalent to eqfnfv . (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Assertion mpteqb 
|- ( A. x e. A B e. V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( B e. V -> B e. _V )
2 1 ralimi 
 |-  ( A. x e. A B e. V -> A. x e. A B e. _V )
3 fneq1 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( ( x e. A |-> B ) Fn A <-> ( x e. A |-> C ) Fn A ) )
4 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
5 4 mptfng 
 |-  ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )
6 eqid 
 |-  ( x e. A |-> C ) = ( x e. A |-> C )
7 6 mptfng 
 |-  ( A. x e. A C e. _V <-> ( x e. A |-> C ) Fn A )
8 3 5 7 3bitr4g 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V <-> A. x e. A C e. _V ) )
9 8 biimpd 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V -> A. x e. A C e. _V ) )
10 r19.26 
 |-  ( A. x e. A ( B e. _V /\ C e. _V ) <-> ( A. x e. A B e. _V /\ A. x e. A C e. _V ) )
11 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
12 nfmpt1 
 |-  F/_ x ( x e. A |-> C )
13 11 12 nfeq 
 |-  F/ x ( x e. A |-> B ) = ( x e. A |-> C )
14 simpll 
 |-  ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
15 14 fveq1d 
 |-  ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( ( x e. A |-> B ) ` x ) = ( ( x e. A |-> C ) ` x ) )
16 4 fvmpt2 
 |-  ( ( x e. A /\ B e. _V ) -> ( ( x e. A |-> B ) ` x ) = B )
17 16 ad2ant2lr 
 |-  ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( ( x e. A |-> B ) ` x ) = B )
18 6 fvmpt2 
 |-  ( ( x e. A /\ C e. _V ) -> ( ( x e. A |-> C ) ` x ) = C )
19 18 ad2ant2l 
 |-  ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> ( ( x e. A |-> C ) ` x ) = C )
20 15 17 19 3eqtr3d 
 |-  ( ( ( ( x e. A |-> B ) = ( x e. A |-> C ) /\ x e. A ) /\ ( B e. _V /\ C e. _V ) ) -> B = C )
21 20 exp31 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( x e. A -> ( ( B e. _V /\ C e. _V ) -> B = C ) ) )
22 13 21 ralrimi 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> A. x e. A ( ( B e. _V /\ C e. _V ) -> B = C ) )
23 ralim 
 |-  ( A. x e. A ( ( B e. _V /\ C e. _V ) -> B = C ) -> ( A. x e. A ( B e. _V /\ C e. _V ) -> A. x e. A B = C ) )
24 22 23 syl 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A ( B e. _V /\ C e. _V ) -> A. x e. A B = C ) )
25 10 24 syl5bir 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( ( A. x e. A B e. _V /\ A. x e. A C e. _V ) -> A. x e. A B = C ) )
26 25 expd 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V -> ( A. x e. A C e. _V -> A. x e. A B = C ) ) )
27 9 26 mpdd 
 |-  ( ( x e. A |-> B ) = ( x e. A |-> C ) -> ( A. x e. A B e. _V -> A. x e. A B = C ) )
28 27 com12 
 |-  ( A. x e. A B e. _V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) -> A. x e. A B = C ) )
29 eqid 
 |-  A = A
30 mpteq12 
 |-  ( ( A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) )
31 29 30 mpan 
 |-  ( A. x e. A B = C -> ( x e. A |-> B ) = ( x e. A |-> C ) )
32 28 31 impbid1 
 |-  ( A. x e. A B e. _V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )
33 2 32 syl 
 |-  ( A. x e. A B e. V -> ( ( x e. A |-> B ) = ( x e. A |-> C ) <-> A. x e. A B = C ) )