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

Theorem in0 4111
Description: The intersection of a class with the empty set is the empty set. Theorem 16 of [Suppes] p. 26. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
in0 (𝐴 ∩ ∅) = ∅

Proof of Theorem in0
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 noel 4062 . . . 4 ¬ 𝑥 ∈ ∅
21bianfi 1004 . . 3 (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 214 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
43ineqri 3949 1 (𝐴 ∩ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1632  wcel 2139  cin 3714  c0 4058
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-nul 4059
This theorem is referenced by:  0in  4112  csbin  4153  res0  5555  fresaun  6236  oev2  7772  cda0en  9193  ackbij1lem13  9246  ackbij1lem16  9249  incexclem  14767  bitsinv1  15366  bitsinvp1  15373  sadcadd  15382  sadadd2  15384  sadid1  15392  bitsres  15397  smumullem  15416  ressbas  16132  sylow2a  18234  ablfac1eu  18672  indistopon  21007  fctop  21010  cctop  21012  rest0  21175  filconn  21888  volinun  23514  itg2cnlem2  23728  pthdlem2  26874  0pth  27277  1pthdlem2  27288  disjdifprg  29695  disjun0  29715  ofpreima2  29775  ldgenpisyslem1  30535  0elcarsg  30678  carsgclctunlem1  30688  carsgclctunlem3  30691  ballotlemfval0  30866  dfpo2  31952  elima4  31984  bj-rest10  33347  bj-rest0  33352  mblfinlem2  33760  conrel1d  38457  conrel2d  38458  ntrk0kbimka  38839  clsneibex  38902  neicvgbex  38912  qinioo  40265  nnfoctbdjlem  41175  caragen0  41226
  Copyright terms: Public domain W3C validator