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

Theorem in0 3646
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 3625 . . . 4  |-  -.  x  e.  (/)
21bianfi 892 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 194 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3527 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1652    e. wcel 1725    i^i cin 3312   (/)c0 3621
This theorem is referenced by:  res0  5143  fresaun  5607  fnsuppeq0  5946  oev2  6760  cda0en  8052  ackbij1lem13  8105  ackbij1lem16  8108  incexclem  12609  bitsinv1  12947  bitsinvp1  12954  sadcadd  12963  sadadd2  12965  sadid1  12973  bitsres  12978  smumullem  12997  ressbas  13512  sylow2a  15246  ablfac1eu  15624  indistopon  17058  fctop  17061  cctop  17063  rest0  17226  restsn  17227  filcon  17908  volinun  19433  itg2cnlem2  19647  chtdif  20934  ppidif  20939  ppi1  20940  cht1  20941  0pth  21563  1pthonlem2  21583  disjdifprg  24010  measvuni  24561  measinb  24568  sibfof  24647  cndprobnul  24688  ballotlemfp1  24742  ballotlemfval0  24746  ballotlemgun  24775  dfpo2  25371  elima4  25397  pred0  25467  mblfinlem  26235
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-dif 3316  df-in 3320  df-nul 3622
  Copyright terms: Public domain W3C validator