Theorem xpeq0

Description: At least one member of an empty Cartesian product is empty. (Contributed by NM, 27-Aug-2006)

	Ref	Expression
Assertion	xpeq0	⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		xpnz	⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
2	1	necon2bbii	⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ¬ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) )
3		ianor	⊢ ( ¬ ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( ¬ 𝐴 ≠ ∅ ∨ ¬ 𝐵 ≠ ∅ ) )
4		nne	⊢ ( ¬ 𝐴 ≠ ∅ ↔ 𝐴 = ∅ )
5		nne	⊢ ( ¬ 𝐵 ≠ ∅ ↔ 𝐵 = ∅ )
6	4 5	orbi12i	⊢ ( ( ¬ 𝐴 ≠ ∅ ∨ ¬ 𝐵 ≠ ∅ ) ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )
7	2 3 6	3bitri	⊢ ( ( 𝐴 × 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) )