Theorem 0in 4349

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

Step	Hyp	Ref	Expression
1		incom 4180	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4347	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2846	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1537   ∩ cin 3937  ∅c0 4293

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-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-in 3945  df-nul 4294

This theorem is referenced by:  pred0  6180  fresaunres2  6552  fnsuppeq0  7860  setsfun  16520  setsfun0  16521  indistopon  21611  fctop  21614  cctop  21616  restsn  21780  filconn  22493  chtdif  25737  ppidif  25742  ppi1  25743  cht1  25744  0res  30356  ofpreima2  30413  ordtconnlem1  31169  measvuni  31475  measinb  31482  cndprobnul  31697  ballotlemfp1  31751  ballotlemgun  31784  chtvalz  31902  mrsubvrs  32771  mblfinlem2  34932  ntrkbimka  40395  neicvgbex  40469  limsup0  41982  subsalsal  42649  nnfoctbdjlem  42744