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

Metamath Proof Explorer

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