Theorem 0in 4351

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 4163	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4349	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2760	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∩ cin 3902  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-nul 4288

This theorem is referenced by:  pred0  6301  fresaunres2  6714  fnsuppeq0  8144  setsfun  17110  setsfun0  17111  indistopon  22957  fctop  22960  cctop  22962  restsn  23126  filconn  23839  chtdif  27136  ppidif  27141  ppi1  27142  cht1  27143  0res  32689  ofpreima2  32755  ordtconnlem1  34101  measvuni  34391  measinb  34398  cndprobnul  34614  ballotlemfp1  34669  ballotlemgun  34702  chtvalz  34806  mrsubvrs  35735  mblfinlem2  37906  ntrkbimka  44391  neicvgbex  44465  limsup0  46049  subsalsal  46714  nnfoctbdjlem  46810  setc1onsubc  49958