Theorem 0nelxp 5645

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 3440	. . . . . . 7 ⊢ 𝑥 ∈ V
2		vex 3440	. . . . . . 7 ⊢ 𝑦 ∈ V
3	1, 2	opnzi 5409	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ≠ ∅
4	3	nesymi 2985	. . . . 5 ⊢ ¬ ∅ = ⟨𝑥, 𝑦⟩
5	4	intnanr 487	. . . 4 ⊢ ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
6	5	nex 1801	. . 3 ⊢ ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
7	6	nex 1801	. 2 ⊢ ¬ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
8		elxp 5634	. 2 ⊢ (∅ ∈ (𝐴 × 𝐵) ↔ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	7, 8	mtbir 323	1 ⊢ ¬ ∅ ∈ (𝐴 × 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∅c0 4278  ⟨cop 4577   × cxp 5609

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-opab 5149  df-xp 5617

This theorem is referenced by:  0nelrel0  5671  nrelv  5735  dmsn0  6151  onxpdisj  6428  mpoxopx0ov0  8141  dmtpos  8163  0nnq  10810  adderpq  10842  mulerpq  10843  lterpq  10856  0ncn  11019  structcnvcnv  17059  vtxval0  29012  iedgval0  29013  msrrcl  35579  oppfrcl2  49161  eloppf  49165