Theorem 0in 4346

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 4158	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4344	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2756	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1541   ∩ cin 3897  ∅c0 4282

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905  df-nul 4283

This theorem is referenced by:  pred0  6289  fresaunres2  6702  fnsuppeq0  8130  setsfun  17086  setsfun0  17087  indistopon  22919  fctop  22922  cctop  22924  restsn  23088  filconn  23801  chtdif  27098  ppidif  27103  ppi1  27104  cht1  27105  0res  32587  ofpreima2  32652  ordtconnlem1  33960  measvuni  34250  measinb  34257  cndprobnul  34473  ballotlemfp1  34528  ballotlemgun  34561  chtvalz  34665  mrsubvrs  35589  mblfinlem2  37721  ntrkbimka  44158  neicvgbex  44232  limsup0  45819  subsalsal  46484  nnfoctbdjlem  46580  setc1onsubc  49730