Theorem 0in 4347

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

Syntax hints:   = wceq 1541   ∩ cin 3901  ∅c0 4283

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 3905  df-in 3909  df-nul 4284

This theorem is referenced by:  pred0  6282  fresaunres2  6695  fnsuppeq0  8122  setsfun  17082  setsfun0  17083  indistopon  22917  fctop  22920  cctop  22922  restsn  23086  filconn  23799  chtdif  27096  ppidif  27101  ppi1  27102  cht1  27103  0res  32581  ofpreima2  32646  ordtconnlem1  33935  measvuni  34225  measinb  34232  cndprobnul  34448  ballotlemfp1  34503  ballotlemgun  34536  chtvalz  34640  mrsubvrs  35564  mblfinlem2  37704  ntrkbimka  44077  neicvgbex  44151  limsup0  45738  subsalsal  46403  nnfoctbdjlem  46499  setc1onsubc  49640