Theorem 0in 4327

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 4135	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4325	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2766	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1539   ∩ cin 3886  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-in 3894  df-nul 4257

This theorem is referenced by:  pred0  6238  fresaunres2  6646  fnsuppeq0  8008  setsfun  16872  setsfun0  16873  indistopon  22151  fctop  22154  cctop  22156  restsn  22321  filconn  23034  chtdif  26307  ppidif  26312  ppi1  26313  cht1  26314  0res  30943  ofpreima2  31003  ordtconnlem1  31874  measvuni  32182  measinb  32189  cndprobnul  32404  ballotlemfp1  32458  ballotlemgun  32491  chtvalz  32609  mrsubvrs  33484  mblfinlem2  35815  ntrkbimka  41648  neicvgbex  41722  limsup0  43235  subsalsal  43898  nnfoctbdjlem  43993