This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpeq0

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

Ref Expression
Assertion xpeq0 ⊢ A × B = ∅ ↔ A = ∅ ∨ B = ∅

Proof

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