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

Theorem in0 3480
Description: The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 5-Aug-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 3459 . . . 4  |-  -.  x  e.  (/)
21bianfi 891 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 193 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3362 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1623    e. wcel 1684    i^i cin 3151   (/)c0 3455
This theorem is referenced by:  res0  4959  fresaun  5412  fnsuppeq0  5733  oev2  6522  cda0en  7805  ackbij1lem13  7858  ackbij1lem16  7861  incexclem  12295  bitsinv1  12633  bitsinvp1  12640  sadcadd  12649  sadadd2  12651  sadid1  12659  bitsres  12664  smumullem  12683  ressbas  13198  sylow2a  14930  ablfac1eu  15308  indistopon  16738  fctop  16741  cctop  16743  rest0  16900  restsn  16901  filcon  17578  volinun  18903  itg2cnlem2  19117  chtdif  20396  ppidif  20401  ppi1  20402  cht1  20403  ballotlemfp1  23050  ballotlemfval0  23054  ballotlemgun  23083  disjdifprg  23352  measvuni  23542  measinb  23548  cndprobnul  23640  dfpo2  24112  pred0  24199  neiopne  25051  hdrmp  25706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-nul 3456
  Copyright terms: Public domain W3C validator