# 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 ${⊢}¬\varnothing \in \left({A}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 vex ${⊢}{x}\in \mathrm{V}$
2 vex ${⊢}{y}\in \mathrm{V}$
3 1 2 opnzi ${⊢}⟨{x},{y}⟩\ne \varnothing$
4 3 nesymi ${⊢}¬\varnothing =⟨{x},{y}⟩$
5 4 intnanr ${⊢}¬\left(\varnothing =⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)$
6 5 nex ${⊢}¬\exists {y}\phantom{\rule{.4em}{0ex}}\left(\varnothing =⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)$
7 6 nex ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\varnothing =⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)$
8 elxp ${⊢}\varnothing \in \left({A}×{B}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left(\varnothing =⟨{x},{y}⟩\wedge \left({x}\in {A}\wedge {y}\in {B}\right)\right)$
9 7 8 mtbir ${⊢}¬\varnothing \in \left({A}×{B}\right)$