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

Theorem 0in 3921
 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 3767 . 2 (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2 in0 3920 . 2 (𝐴 ∩ ∅) = ∅
31, 2eqtri 2632 1 (∅ ∩ 𝐴) = ∅
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∩ cin 3539  ∅c0 3874 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-nul 3875 This theorem is referenced by:  pred0  5627  fnsuppeq0  7210  setsfun  15725  setsfun0  15726  indistopon  20615  fctop  20618  cctop  20620  restsn  20784  filcon  21497  chtdif  24684  ppidif  24689  ppi1  24690  cht1  24691  ofpreima2  28849  ordtconlem1  29298  measvuni  29604  measinb  29611  cndprobnul  29826  ballotlemfp1  29880  ballotlemgun  29913  mrsubvrs  30673  mblfinlem2  32617  subsalsal  39253  nnfoctbdjlem  39348
 Copyright terms: Public domain W3C validator