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

Theorem 0in 4002
 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 3838 . 2 (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2 in0 4001 . 2 (𝐴 ∩ ∅) = ∅
31, 2eqtri 2673 1 (∅ ∩ 𝐴) = ∅
 Colors of variables: wff setvar class Syntax hints:   = wceq 1523   ∩ cin 3606  ∅c0 3948 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-nul 3949 This theorem is referenced by:  pred0  5748  fnsuppeq0  7368  setsfun  15940  setsfun0  15941  indistopon  20853  fctop  20856  cctop  20858  restsn  21022  filconn  21734  chtdif  24929  ppidif  24934  ppi1  24935  cht1  24936  ofpreima2  29594  ordtconnlem1  30098  measvuni  30405  measinb  30412  cndprobnul  30627  ballotlemfp1  30681  ballotlemgun  30714  chtvalz  30835  mrsubvrs  31545  mblfinlem2  33577  ntrkbimka  38653  limsup0  40244  subsalsal  40895  nnfoctbdjlem  40990
 Copyright terms: Public domain W3C validator