Description: The empty set is not a member of a Cartesian product. (Contributed by NM, 2-May-1996) (Revised by Mario Carneiro, 26-Apr-2015) (Proof shortened by JJ, 13-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | 0nelxp | ⊢ ¬ ∅ ∈ ( 𝐴 × 𝐵 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | ⊢ 𝑥 ∈ V | |
2 | vex | ⊢ 𝑦 ∈ V | |
3 | 1 2 | opnzi | ⊢ 〈 𝑥 , 𝑦 〉 ≠ ∅ |
4 | 3 | nesymi | ⊢ ¬ ∅ = 〈 𝑥 , 𝑦 〉 |
5 | 4 | intnanr | ⊢ ¬ ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
6 | 5 | nex | ⊢ ¬ ∃ 𝑦 ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
7 | 6 | nex | ⊢ ¬ ∃ 𝑥 ∃ 𝑦 ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
8 | elxp | ⊢ ( ∅ ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ∅ = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ) | |
9 | 7 8 | mtbir | ⊢ ¬ ∅ ∈ ( 𝐴 × 𝐵 ) |