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

Theorem 0in 4395
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 4199 . 2 (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2 in0 4393 . 2 (𝐴 ∩ ∅) = ∅
31, 2eqtri 2753 1 (∅ ∩ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  cin 3943  c0 4322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-in 3951  df-nul 4323
This theorem is referenced by:  pred0  6343  fresaunres2  6769  fnsuppeq0  8197  setsfun  17143  setsfun0  17144  indistopon  22948  fctop  22951  cctop  22953  restsn  23118  filconn  23831  chtdif  27135  ppidif  27140  ppi1  27141  cht1  27142  0res  32472  ofpreima2  32533  ordtconnlem1  33656  measvuni  33964  measinb  33971  cndprobnul  34188  ballotlemfp1  34242  ballotlemgun  34275  chtvalz  34392  mrsubvrs  35263  mblfinlem2  37262  ntrkbimka  43610  neicvgbex  43684  limsup0  45220  subsalsal  45885  nnfoctbdjlem  45981
  Copyright terms: Public domain W3C validator