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	$$⊢\neg \varnothing \in \left(A\times 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	$$⊢\neg \varnothing =⟨x,y⟩$$
5	4	intnanr	$$⊢\neg \left(\varnothing =⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)$$
6	5	nex	$$⊢\neg \exists y\left(\varnothing =⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)$$
7	6	nex	$$⊢\neg \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)$$
8		elxp	$$⊢\varnothing \in \left(A\times B\right)\leftrightarrow \exists x\exists y\left(\varnothing =⟨x,y⟩\wedge \left(x\in A\wedge y\in B\right)\right)$$
9	7 8	mtbir	$$⊢\neg \varnothing \in \left(A\times B\right)$$