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

Theorem in0 4344
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 4295 . . . 4 ¬ 𝑥 ∈ ∅
21bianfi 534 . . 3 (𝑥 ∈ ∅ ↔ (𝑥𝐴𝑥 ∈ ∅))
32bicomi 225 . 2 ((𝑥𝐴𝑥 ∈ ∅) ↔ 𝑥 ∈ ∅)
43ineqri 4179 1 (𝐴 ∩ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:  wa 396   = wceq 1528  wcel 2105  cin 3934  c0 4290
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-in 3942  df-nul 4291
This theorem is referenced by:  0in  4346  csbin  4390  res0  5851  fresaun  6543  oev2  8139  dju0en  9590  ackbij1lem13  9643  ackbij1lem16  9646  incexclem  15181  bitsinv1  15781  bitsinvp1  15788  sadcadd  15797  sadadd2  15799  sadid1  15807  bitsres  15812  smumullem  15831  ressbas  16544  sylow2a  18675  ablfac1eu  19126  indistopon  21539  fctop  21542  cctop  21544  rest0  21707  filconn  22421  volinun  24076  itg2cnlem2  24292  pthdlem2  27477  0pth  27832  1pthdlem2  27843  disjdifprg  30254  disjun0  30274  ofpreima2  30340  ldgenpisyslem1  31322  0elcarsg  31465  carsgclctunlem1  31475  carsgclctunlem3  31478  ballotlemfval0  31653  sate0  32560  dfpo2  32889  elima4  32917  bj-rest10  34274  bj-rest0  34279  mblfinlem2  34812  conrel1d  39888  conrel2d  39889  ntrk0kbimka  40269  clsneibex  40332  neicvgbex  40342  qinioo  41691  nnfoctbdjlem  42618  caragen0  42669
  Copyright terms: Public domain W3C validator