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

Theorem in0 4348
 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 4299 . . . 4 ¬ 𝑥 ∈ ∅
21bianfi 534 . . 3 (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 225 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
43ineqri 4183 1 (𝐴 ∩ ∅) = ∅
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 396   = wceq 1530   ∈ wcel 2106   ∩ cin 3938  ∅c0 4294 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-v 3501  df-dif 3942  df-in 3946  df-nul 4295 This theorem is referenced by:  0in  4350  csbin  4394  res0  5855  fresaun  6545  oev2  8142  dju0en  9593  ackbij1lem13  9646  ackbij1lem16  9649  incexclem  15183  bitsinv1  15783  bitsinvp1  15790  sadcadd  15799  sadadd2  15801  sadid1  15809  bitsres  15814  smumullem  15833  ressbas  16546  sylow2a  18666  ablfac1eu  19117  indistopon  21525  fctop  21528  cctop  21530  rest0  21693  filconn  22407  volinun  24062  itg2cnlem2  24278  pthdlem2  27464  0pth  27819  1pthdlem2  27830  disjdifprg  30241  disjun0  30261  ofpreima2  30327  ldgenpisyslem1  31309  0elcarsg  31452  carsgclctunlem1  31462  carsgclctunlem3  31465  ballotlemfval0  31640  sate0  32547  dfpo2  32876  elima4  32904  bj-rest10  34261  bj-rest0  34266  mblfinlem2  34798  conrel1d  39870  conrel2d  39871  ntrk0kbimka  40251  clsneibex  40314  neicvgbex  40324  qinioo  41673  nnfoctbdjlem  42600  caragen0  42651
 Copyright terms: Public domain W3C validator