Theorem 0in 4393

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

Syntax hints:   = wceq 1541   ∩ cin 3947  ∅c0 4322

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-in 3955  df-nul 4323

This theorem is referenced by:  pred0  6336  fresaunres2  6763  fnsuppeq0  8176  setsfun  17103  setsfun0  17104  indistopon  22503  fctop  22506  cctop  22508  restsn  22673  filconn  23386  chtdif  26659  ppidif  26664  ppi1  26665  cht1  26666  0res  31829  ofpreima2  31886  ordtconnlem1  32899  measvuni  33207  measinb  33214  cndprobnul  33431  ballotlemfp1  33485  ballotlemgun  33518  chtvalz  33636  mrsubvrs  34508  mblfinlem2  36521  ntrkbimka  42779  neicvgbex  42853  limsup0  44400  subsalsal  45065  nnfoctbdjlem  45161