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

Theorem in0 3617
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 3596 . . . 4  |-  -.  x  e.  (/)
21bianfi 892 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 194 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3498 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 359    = wceq 1649    e. wcel 1721    i^i cin 3283   (/)c0 3592
This theorem is referenced by:  res0  5113  fresaun  5577  fnsuppeq0  5916  oev2  6730  cda0en  8019  ackbij1lem13  8072  ackbij1lem16  8075  incexclem  12575  bitsinv1  12913  bitsinvp1  12920  sadcadd  12929  sadadd2  12931  sadid1  12939  bitsres  12944  smumullem  12963  ressbas  13478  sylow2a  15212  ablfac1eu  15590  indistopon  17024  fctop  17027  cctop  17029  rest0  17191  restsn  17192  filcon  17872  volinun  19397  itg2cnlem2  19611  chtdif  20898  ppidif  20903  ppi1  20904  cht1  20905  0pth  21527  1pthonlem2  21547  disjdifprg  23974  measvuni  24525  measinb  24532  sibfof  24611  cndprobnul  24652  ballotlemfp1  24706  ballotlemfval0  24710  ballotlemgun  24739  dfpo2  25330  pred0  25417  mblfinlem  26147
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-v 2922  df-dif 3287  df-in 3291  df-nul 3593
  Copyright terms: Public domain W3C validator