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 4161	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4347	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2759	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1541   ∩ cin 3900  ∅c0 4285

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-in 3908  df-nul 4286

This theorem is referenced by:  pred0  6293  fresaunres2  6706  fnsuppeq0  8134  setsfun  17098  setsfun0  17099  indistopon  22945  fctop  22948  cctop  22950  restsn  23114  filconn  23827  chtdif  27124  ppidif  27129  ppi1  27130  cht1  27131  0res  32678  ofpreima2  32744  ordtconnlem1  34081  measvuni  34371  measinb  34378  cndprobnul  34594  ballotlemfp1  34649  ballotlemgun  34682  chtvalz  34786  mrsubvrs  35716  mblfinlem2  37859  ntrkbimka  44279  neicvgbex  44353  limsup0  45938  subsalsal  46603  nnfoctbdjlem  46699  setc1onsubc  49847