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

Theorem in0 3598
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 3577 . . . 4  |-  -.  x  e.  (/)
21bianfi 892 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 194 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3479 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1649    e. wcel 1717    i^i cin 3264   (/)c0 3573
This theorem is referenced by:  res0  5092  fresaun  5556  fnsuppeq0  5894  oev2  6705  cda0en  7994  ackbij1lem13  8047  ackbij1lem16  8050  incexclem  12545  bitsinv1  12883  bitsinvp1  12890  sadcadd  12899  sadadd2  12901  sadid1  12909  bitsres  12914  smumullem  12933  ressbas  13448  sylow2a  15182  ablfac1eu  15560  indistopon  16990  fctop  16993  cctop  16995  rest0  17157  restsn  17158  filcon  17838  volinun  19309  itg2cnlem2  19523  chtdif  20810  ppidif  20815  ppi1  20816  cht1  20817  0pth  21426  1pthonlem2  21440  disjdifprg  23863  measvuni  24364  measinb  24371  cndprobnul  24476  ballotlemfp1  24530  ballotlemfval0  24534  ballotlemgun  24563  dfpo2  25138  pred0  25225
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-v 2903  df-dif 3268  df-in 3272  df-nul 3574
  Copyright terms: Public domain W3C validator