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