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 ) )