Theorem xpcomeng

Description: Commutative law for equinumerosity of Cartesian product. Proposition 4.22(d) of Mendelson p. 254. (Contributed by NM, 27-Mar-2006)

	Ref	Expression
Assertion	xpcomeng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xpeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 × 𝑦 ) = ( 𝐴 × 𝑦 ) )
2		xpeq2	⊢ ( 𝑥 = 𝐴 → ( 𝑦 × 𝑥 ) = ( 𝑦 × 𝐴 ) )
3	1 2	breq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 × 𝑦 ) ≈ ( 𝑦 × 𝑥 ) ↔ ( 𝐴 × 𝑦 ) ≈ ( 𝑦 × 𝐴 ) ) )
4		xpeq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 × 𝑦 ) = ( 𝐴 × 𝐵 ) )
5		xpeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 × 𝐴 ) = ( 𝐵 × 𝐴 ) )
6	4 5	breq12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 × 𝑦 ) ≈ ( 𝑦 × 𝐴 ) ↔ ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) ) )
7		vex	⊢ 𝑥 ∈ V
8		vex	⊢ 𝑦 ∈ V
9	7 8	xpcomen	⊢ ( 𝑥 × 𝑦 ) ≈ ( 𝑦 × 𝑥 )
10	3 6 9	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )