Theorem 0in 4344

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 4156	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4342	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2754	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1541   ∩ cin 3896  ∅c0 4280

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-in 3904  df-nul 4281

This theorem is referenced by:  pred0  6282  fresaunres2  6695  fnsuppeq0  8122  setsfun  17082  setsfun0  17083  indistopon  22916  fctop  22919  cctop  22921  restsn  23085  filconn  23798  chtdif  27095  ppidif  27100  ppi1  27101  cht1  27102  0res  32583  ofpreima2  32648  ordtconnlem1  33937  measvuni  34227  measinb  34234  cndprobnul  34450  ballotlemfp1  34505  ballotlemgun  34538  chtvalz  34642  mrsubvrs  35566  mblfinlem2  37697  ntrkbimka  44130  neicvgbex  44204  limsup0  45791  subsalsal  46456  nnfoctbdjlem  46552  setc1onsubc  49702