Metamath Proof Explorer


Theorem 0nelxp

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 ¬ ∅ ∈ ( 𝐴 × 𝐵 )

Proof

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 ¬ ∅ ∈ ( 𝐴 × 𝐵 )