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

Theorem in0 3481
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  (/) )  =  (/)
Dummy variable  x is distinct from all other variables.

Proof of Theorem in0
StepHypRef Expression
1 noel 3460 . . . 4  |-  -.  x  e.  (/)
21bianfi 893 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 195 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3363 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1624    e. wcel 1685    i^i cin 3152   (/)c0 3456
This theorem is referenced by:  res0  4958  fresaun  5377  fnsuppeq0  5694  oev2  6517  cda0en  7800  ackbij1lem13  7853  ackbij1lem16  7856  incexclem  12289  bitsinv1  12627  bitsinvp1  12634  sadcadd  12643  sadadd2  12645  sadid1  12653  bitsres  12658  smumullem  12677  ressbas  13192  sylow2a  14924  ablfac1eu  15302  indistopon  16732  fctop  16735  cctop  16737  rest0  16894  restsn  16895  filcon  17572  volinun  18897  itg2cnlem2  19111  chtdif  20390  ppidif  20395  ppi1  20396  cht1  20397  ballotlemfp1  23043  ballotlemfval0  23047  ballotlemgun  23076  dfpo2  23515  pred0  23600  neiopne  24449  hdrmp  25105
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-in 3160  df-nul 3457
  Copyright terms: Public domain W3C validator