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

Theorem in0 4342
Description: The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
in0 (𝐴 ∩ ∅) = ∅

Proof of Theorem in0
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 noel 4293 . . . 4 ¬ 𝑥 ∈ ∅
21bianfi 534 . . 3 (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 225 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
43ineqri 4177 1 (𝐴 ∩ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wcel 2105  cin 3932  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936  df-in 3940  df-nul 4289
This theorem is referenced by:  0in  4344  csbin  4388  res0  5850  fresaun  6542  oev2  8137  dju0en  9589  ackbij1lem13  9642  ackbij1lem16  9645  incexclem  15179  bitsinv1  15779  bitsinvp1  15786  sadcadd  15795  sadadd2  15797  sadid1  15805  bitsres  15810  smumullem  15829  ressbas  16542  sylow2a  18673  ablfac1eu  19124  indistopon  21537  fctop  21540  cctop  21542  rest0  21705  filconn  22419  volinun  24074  itg2cnlem2  24290  pthdlem2  27476  0pth  27831  1pthdlem2  27842  disjdifprg  30253  disjun0  30273  ofpreima2  30339  ldgenpisyslem1  31321  0elcarsg  31464  carsgclctunlem1  31474  carsgclctunlem3  31477  ballotlemfval0  31652  sate0  32559  dfpo2  32888  elima4  32916  bj-rest10  34273  bj-rest0  34278  mblfinlem2  34811  conrel1d  39886  conrel2d  39887  ntrk0kbimka  40267  clsneibex  40330  neicvgbex  40340  qinioo  41687  nnfoctbdjlem  42614  caragen0  42665
  Copyright terms: Public domain W3C validator