Theorem cnvxp

Description: The converse of a Cartesian product. Exercise 11 of Suppes p. 67. (Contributed by NM, 14-Aug-1999) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	cnvxp	|- `' ( A X. B ) = ( B X. A )

Proof

Step	Hyp	Ref	Expression
1		cnvopab	|- `' { <. y , x >. | ( y e. A /\ x e. B ) } = { <. x , y >. | ( y e. A /\ x e. B ) }
2		ancom	|- ( ( y e. A /\ x e. B ) <-> ( x e. B /\ y e. A ) )
3	2	opabbii	|- { <. x , y >. | ( y e. A /\ x e. B ) } = { <. x , y >. | ( x e. B /\ y e. A ) }
4	1 3	eqtri	|- `' { <. y , x >. | ( y e. A /\ x e. B ) } = { <. x , y >. | ( x e. B /\ y e. A ) }
5		df-xp	|- ( A X. B ) = { <. y , x >. | ( y e. A /\ x e. B ) }
6	5	cnveqi	|- `' ( A X. B ) = `' { <. y , x >. | ( y e. A /\ x e. B ) }
7		df-xp	|- ( B X. A ) = { <. x , y >. | ( x e. B /\ y e. A ) }
8	4 6 7	3eqtr4i	|- `' ( A X. B ) = ( B X. A )