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

Theorem in0 3455
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
StepHypRef Expression
1 noel 3434 . . . 4  |-  -.  x  e.  (/)
21bianfi 896 . . 3  |-  ( x  e.  (/)  <->  ( x  e.  A  /\  x  e.  (/) ) )
32bicomi 195 . 2  |-  ( ( x  e.  A  /\  x  e.  (/) )  <->  x  e.  (/) )
43ineqri 3337 1  |-  ( A  i^i  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 360    = wceq 1619    e. wcel 1621    i^i cin 3126   (/)c0 3430
This theorem is referenced by:  res0  4947  fresaun  5350  fnsuppeq0  5667  oev2  6490  cda0en  7773  ackbij1lem13  7826  ackbij1lem16  7829  bitsinv1  12595  bitsinvp1  12602  sadcadd  12611  sadadd2  12613  sadid1  12621  bitsres  12626  smumullem  12645  ressbas  13160  sylow2a  14892  ablfac1eu  15270  indistopon  16700  fctop  16703  cctop  16705  rest0  16862  restsn  16863  filcon  17540  volinun  18865  itg2cnlem2  19079  chtdif  20358  ppidif  20363  ppi1  20364  cht1  20365  ballotlemfp1  23011  ballotlemfval0  23015  ballotlemgun  23044  dfpo2  23483  pred0  23568  neiopne  24417  hdrmp  25073
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-dif 3130  df-in 3134  df-nul 3431
  Copyright terms: Public domain W3C validator