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

Theorem 0nelxp 5141
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 3201 . . . . . . 7 𝑥 ∈ V
2 vex 3201 . . . . . . 7 𝑦 ∈ V
31, 2opnzi 4941 . . . . . 6 𝑥, 𝑦⟩ ≠ ∅
43nesymi 2850 . . . . 5 ¬ ∅ = ⟨𝑥, 𝑦
54intnanr 961 . . . 4 ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵))
65nex 1730 . . 3 ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵))
76nex 1730 . 2 ¬ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵))
8 elxp 5129 . 2 (∅ ∈ (𝐴 × 𝐵) ↔ ∃𝑥𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥𝐴𝑦𝐵)))
97, 8mtbir 313 1 ¬ ∅ ∈ (𝐴 × 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 384   = wceq 1482  wex 1703  wcel 1989  c0 3913  cop 4181   × cxp 5110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-opab 4711  df-xp 5118
This theorem is referenced by:  0nelrel  5160  nrelv  5242  dmsn0  5600  onxpdisj  5845  nfunv  5919  mpt2xopx0ov0  7339  reldmtpos  7357  dmtpos  7361  0nnq  9743  adderpq  9775  mulerpq  9776  lterpq  9789  0ncn  9951  structcnvcnv  15865  vtxval0  25925  iedgval0  25926  msrrcl  31425  relintabex  37713
  Copyright terms: Public domain W3C validator