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	⊢ ( ( 𝐴 × 𝐵 ) ∈ V ↔ ( 𝐵 × 𝐴 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		cnvxp	⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
2		cnvexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ◡ ( 𝐴 × 𝐵 ) ∈ V )
3	1 2	eqeltrrid	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( 𝐵 × 𝐴 ) ∈ V )
4		cnvxp	⊢ ◡ ( 𝐵 × 𝐴 ) = ( 𝐴 × 𝐵 )
5		cnvexg	⊢ ( ( 𝐵 × 𝐴 ) ∈ V → ◡ ( 𝐵 × 𝐴 ) ∈ V )
6	4 5	eqeltrrid	⊢ ( ( 𝐵 × 𝐴 ) ∈ V → ( 𝐴 × 𝐵 ) ∈ V )
7	3 6	impbii	⊢ ( ( 𝐴 × 𝐵 ) ∈ V ↔ ( 𝐵 × 𝐴 ) ∈ V )