Theorem 0nelxp 5685

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.)

Assertion

Ref	Expression
0nelxp	⊢ ¬ ∅ ∈ (𝐴 × 𝐵)

Proof of Theorem 0nelxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3454	. . . . . . 7 ⊢ 𝑥 ∈ V
2		vex 3454	. . . . . . 7 ⊢ 𝑦 ∈ V
3	1, 2	opnzi 5443	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ≠ ∅
4	3	nesymi 3012	. . . . 5 ⊢ ¬ ∅ = ⟨𝑥, 𝑦⟩
5	4	intnanr 493	. . . 4 ⊢ ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
6	5	nex 1832	. . 3 ⊢ ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
7	6	nex 1832	. 2 ⊢ ¬ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
8		elxp 5674	. 2 ⊢ (∅ ∈ (𝐴 × 𝐵) ↔ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	7, 8	mtbir 326	1 ⊢ ¬ ∅ ∈ (𝐴 × 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∅c0 4277  ⟨cop 4834   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-xp 5657

This theorem is used by:  0nelrel0  5711  nrelvOLD  5779  dmsn0  6213  onxpdisj  6493  mpoxopx0ov0  8241  dmtpos  8263  0nnq  11016  adderpq  11048  mulerpq  11049  lterpq  11062  0ncn  11225  structcnvcnv  17340  vtxval0  29626  iedgval0  29627  msrrcl  36426  oppfrcl2  50381  eloppf  50385