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

Theorem 0in 3946
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 3788 . 2 (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2 in0 3945 . 2 (𝐴 ∩ ∅) = ∅
31, 2eqtri 2648 1 (∅ ∩ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  cin 3559  c0 3896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-dif 3563  df-in 3567  df-nul 3897
This theorem is referenced by:  pred0  5672  fnsuppeq0  7269  setsfun  15809  setsfun0  15810  indistopon  20710  fctop  20713  cctop  20715  restsn  20879  filconn  21592  chtdif  24779  ppidif  24784  ppi1  24785  cht1  24786  ofpreima2  29300  ordtconnlem1  29744  measvuni  30050  measinb  30057  cndprobnul  30272  ballotlemfp1  30326  ballotlemgun  30359  mrsubvrs  31119  mblfinlem2  33065  ntrkbimka  37804  limsup0  39317  subsalsal  39871  nnfoctbdjlem  39966
  Copyright terms: Public domain W3C validator