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

Theorem 0in 4323
 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 4156 . 2 (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2 in0 4321 . 2 (𝐴 ∩ ∅) = ∅
31, 2eqtri 2843 1 (∅ ∩ 𝐴) = ∅
 Colors of variables: wff setvar class Syntax hints:   = wceq 1537   ∩ cin 3912  ∅c0 4269 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792 This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1540  df-ex 1781  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-rab 3134  df-v 3475  df-dif 3916  df-in 3920  df-nul 4270 This theorem is referenced by:  pred0  6154  fresaunres2  6526  fnsuppeq0  7836  setsfun  16497  setsfun0  16498  indistopon  21585  fctop  21588  cctop  21590  restsn  21754  filconn  22467  chtdif  25722  ppidif  25727  ppi1  25728  cht1  25729  0res  30341  ofpreima2  30398  ordtconnlem1  31175  measvuni  31481  measinb  31488  cndprobnul  31703  ballotlemfp1  31757  ballotlemgun  31790  chtvalz  31908  mrsubvrs  32777  mblfinlem2  34971  ntrkbimka  40523  neicvgbex  40597  limsup0  42127  subsalsal  42790  nnfoctbdjlem  42885
 Copyright terms: Public domain W3C validator