Theorem 0in 4403

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 4217	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4401	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2763	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1537   ∩ cin 3962  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-in 3970  df-nul 4340

This theorem is referenced by:  pred0  6358  fresaunres2  6781  fnsuppeq0  8216  setsfun  17205  setsfun0  17206  indistopon  23024  fctop  23027  cctop  23029  restsn  23194  filconn  23907  chtdif  27216  ppidif  27221  ppi1  27222  cht1  27223  0res  32623  ofpreima2  32683  ordtconnlem1  33885  measvuni  34195  measinb  34202  cndprobnul  34419  ballotlemfp1  34473  ballotlemgun  34506  chtvalz  34623  mrsubvrs  35507  mblfinlem2  37645  ntrkbimka  44028  neicvgbex  44102  limsup0  45650  subsalsal  46315  nnfoctbdjlem  46411