Theorem mptcnv

Description: The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017)

	Ref	Expression
Hypothesis	mptcnv.1	|- ( ph -> ( ( x e. A /\ y = B ) <-> ( y e. C /\ x = D ) ) )
Assertion	mptcnv	|- ( ph -> `' ( x e. A |-> B ) = ( y e. C |-> D ) )

Proof

Step	Hyp	Ref	Expression
1		mptcnv.1	|- ( ph -> ( ( x e. A /\ y = B ) <-> ( y e. C /\ x = D ) ) )
2	1	opabbidv	|- ( ph -> { <. y , x >. | ( x e. A /\ y = B ) } = { <. y , x >. | ( y e. C /\ x = D ) } )
3		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
4	3	cnveqi	|- `' ( x e. A |-> B ) = `' { <. x , y >. | ( x e. A /\ y = B ) }
5		cnvopab	|- `' { <. x , y >. | ( x e. A /\ y = B ) } = { <. y , x >. | ( x e. A /\ y = B ) }
6	4 5	eqtri	|- `' ( x e. A |-> B ) = { <. y , x >. | ( x e. A /\ y = B ) }
7		df-mpt	|- ( y e. C |-> D ) = { <. y , x >. | ( y e. C /\ x = D ) }
8	2 6 7	3eqtr4g	|- ( ph -> `' ( x e. A |-> B ) = ( y e. C |-> D ) )