MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0nelxp Structured version   Visualization version   GIF version

Theorem 0nelxp 5576
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.
StepHypRef Expression
1 vex 3483 . . . . . . 7 𝑥 ∈ V
2 vex 3483 . . . . . . 7 𝑦 ∈ V
31, 2opnzi 5353 . . . . . 6 𝑥, 𝑦⟩ ≠ ∅
43nesymi 3071 . . . . 5 ¬ ∅ = ⟨𝑥, 𝑦
54intnanr 491 . . . 4 ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵))
65nex 1802 . . 3 ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵))
76nex 1802 . 2 ¬ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵))
8 elxp 5565 . 2 (∅ ∈ (𝐴 × 𝐵) ↔ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵)))
97, 8mtbir 326 1 ¬ ∅ ∈ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 399   = wceq 1538  wex 1781  wcel 2115  c0 4276  cop 4556   × cxp 5540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5189  ax-nul 5196  ax-pr 5317
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-v 3482  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-sn 4551  df-pr 4553  df-op 4557  df-opab 5115  df-xp 5548
This theorem is referenced by:  0nelrel0  5599  nrelv  5660  dmsn0  6053  onxpdisj  6297  mpoxopx0ov0  7878  dmtpos  7900  0nnq  10344  adderpq  10376  mulerpq  10377  lterpq  10390  0ncn  10553  structcnvcnv  16497  vtxval0  26835  iedgval0  26836  msrrcl  32847
  Copyright terms: Public domain W3C validator