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

Theorem 0in 4354
Description: The intersection of the empty set with a class is the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Assertion
Ref Expression
0in (∅ ∩ 𝐴) = ∅

Proof of Theorem 0in
StepHypRef Expression
1 incom 4162 . 2 (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2 in0 4352 . 2 (𝐴 ∩ ∅) = ∅
31, 2eqtri 2761 1 (∅ ∩ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cin 3910  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-in 3918  df-nul 4284
This theorem is referenced by:  pred0  6290  fresaunres2  6715  fnsuppeq0  8124  setsfun  17048  setsfun0  17049  indistopon  22367  fctop  22370  cctop  22372  restsn  22537  filconn  23250  chtdif  26523  ppidif  26528  ppi1  26529  cht1  26530  0res  31568  ofpreima2  31628  ordtconnlem1  32562  measvuni  32870  measinb  32877  cndprobnul  33094  ballotlemfp1  33148  ballotlemgun  33181  chtvalz  33299  mrsubvrs  34173  mblfinlem2  36162  ntrkbimka  42398  neicvgbex  42472  limsup0  44021  subsalsal  44686  nnfoctbdjlem  44782
  Copyright terms: Public domain W3C validator