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

Theorem in0 3772
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  |-  ( A  i^i  (/) )  =  (/)

Proof of Theorem in0
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 noel 3747 . . . 4  |-  -.  x  e.  (/)
21bianfi 941 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 207 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3638 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 375    = wceq 1455    e. wcel 1898    i^i cin 3415   (/)c0 3743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-dif 3419  df-in 3423  df-nul 3744
This theorem is referenced by:  csbin  3811  res0  5131  pred0  5433  fresaun  5781  fnsuppeq0  6975  oev2  7256  cda0en  8640  ackbij1lem13  8693  ackbij1lem16  8696  incexclem  13949  bitsinv1  14471  bitsinvp1  14478  sadcadd  14487  sadadd2  14489  sadid1  14497  bitsres  14502  smumullem  14521  ressbas  15234  sylow2a  17326  ablfac1eu  17761  indistopon  20071  fctop  20074  cctop  20076  rest0  20240  restsn  20241  filcon  20953  volinun  22555  itg2cnlem2  22776  chtdif  24141  ppidif  24146  ppi1  24147  cht1  24148  0pth  25356  1pthonlem2  25376  disjdifprg  28239  disjun0  28259  ofpreima2  28321  ordtconlem1  28781  ldgenpisyslem1  29036  measvuni  29087  measinb  29094  0elcarsg  29189  carsgclctunlem1  29199  carsgclctunlem3  29202  cndprobnul  29320  ballotlemfp1  29374  ballotlemfval0  29378  ballotlemgun  29407  ballotlemgunOLD  29445  mrsubvrs  30210  dfpo2  30445  elima4  30471  mblfinlem2  32024  conrel1d  36301  conrel2d  36302  0in  37432  qinioo  37722  nnfoctbdjlem  38398  caragen0  38435  pthdlem2  39890  0pth-av  39937  1pthdlem2  39947
  Copyright terms: Public domain W3C validator