Theorem xpexb

Description: A Cartesian product exists iff its converse does. Corollary 6.9(1) in TakeutiZaring p. 26. (Contributed by Andrew Salmon, 13-Nov-2011)

	Ref	Expression
Assertion	xpexb	|- ( ( A X. B ) e. _V <-> ( B X. A ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		cnvxp	|- `' ( A X. B ) = ( B X. A )
2		cnvexg	|- ( ( A X. B ) e. _V -> `' ( A X. B ) e. _V )
3	1 2	eqeltrrid	|- ( ( A X. B ) e. _V -> ( B X. A ) e. _V )
4		cnvxp	|- `' ( B X. A ) = ( A X. B )
5		cnvexg	|- ( ( B X. A ) e. _V -> `' ( B X. A ) e. _V )
6	4 5	eqeltrrid	|- ( ( B X. A ) e. _V -> ( A X. B ) e. _V )
7	3 6	impbii	|- ( ( A X. B ) e. _V <-> ( B X. A ) e. _V )