Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of Monk1 p. 37. (Contributed by NM, 12-Apr-2004) Avoid axioms. (Revised by TM, 1-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | xp0 | ⊢ ( 𝐴 × ∅ ) = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noel | ⊢ ¬ 𝑦 ∈ ∅ | |
| 2 | simprr | ⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅ ) ) → 𝑦 ∈ ∅ ) | |
| 3 | 1 2 | mto | ⊢ ¬ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅ ) ) |
| 4 | 3 | nex | ⊢ ¬ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅ ) ) |
| 5 | 4 | nex | ⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅ ) ) |
| 6 | elxpi | ⊢ ( 𝑧 ∈ ( 𝐴 × ∅ ) → ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∅ ) ) ) | |
| 7 | 5 6 | mto | ⊢ ¬ 𝑧 ∈ ( 𝐴 × ∅ ) |
| 8 | 7 | nel0 | ⊢ ( 𝐴 × ∅ ) = ∅ |