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

Metamath Proof Explorer

Theorem mpteq12f

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013)

Ref Expression
Assertion mpteq12f 
|- ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x A = C
2 nfra1 
 |-  F/ x A. x e. A B = D
3 1 2 nfan 
 |-  F/ x ( A. x A = C /\ A. x e. A B = D )
4 nfv 
 |-  F/ y ( A. x A = C /\ A. x e. A B = D )
5 rspa 
 |-  ( ( A. x e. A B = D /\ x e. A ) -> B = D )
6 5 eqeq2d 
 |-  ( ( A. x e. A B = D /\ x e. A ) -> ( y = B <-> y = D ) )
7 6 pm5.32da 
 |-  ( A. x e. A B = D -> ( ( x e. A /\ y = B ) <-> ( x e. A /\ y = D ) ) )
8 sp 
 |-  ( A. x A = C -> A = C )
9 8 eleq2d 
 |-  ( A. x A = C -> ( x e. A <-> x e. C ) )
10 9 anbi1d 
 |-  ( A. x A = C -> ( ( x e. A /\ y = D ) <-> ( x e. C /\ y = D ) ) )
11 7 10 sylan9bbr 
 |-  ( ( A. x A = C /\ A. x e. A B = D ) -> ( ( x e. A /\ y = B ) <-> ( x e. C /\ y = D ) ) )
12 3 4 11 opabbid 
 |-  ( ( A. x A = C /\ A. x e. A B = D ) -> { <. x , y >. | ( x e. A /\ y = B ) } = { <. x , y >. | ( x e. C /\ y = D ) } )
13 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
14 df-mpt 
 |-  ( x e. C |-> D ) = { <. x , y >. | ( x e. C /\ y = D ) }
15 12 13 14 3eqtr4g 
 |-  ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )