Theorem 0in 4372

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 4184	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4370	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2758	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1540   ∩ cin 3925  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-in 3933  df-nul 4309

This theorem is referenced by:  pred0  6324  fresaunres2  6750  fnsuppeq0  8191  setsfun  17190  setsfun0  17191  indistopon  22939  fctop  22942  cctop  22944  restsn  23108  filconn  23821  chtdif  27120  ppidif  27125  ppi1  27126  cht1  27127  0res  32584  ofpreima2  32644  ordtconnlem1  33955  measvuni  34245  measinb  34252  cndprobnul  34469  ballotlemfp1  34524  ballotlemgun  34557  chtvalz  34661  mrsubvrs  35544  mblfinlem2  37682  ntrkbimka  44062  neicvgbex  44136  limsup0  45723  subsalsal  46388  nnfoctbdjlem  46484  setc1onsubc  49479