Theorem 0in 4333

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 4140	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4331	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2768	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∩ cin 3891  ∅c0 4262

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-in 3899  df-nul 4263

This theorem is referenced by:  pred0  6237  fresaunres2  6644  fnsuppeq0  7999  setsfun  16870  setsfun0  16871  indistopon  22149  fctop  22152  cctop  22154  restsn  22319  filconn  23032  chtdif  26305  ppidif  26310  ppi1  26311  cht1  26312  0res  30939  ofpreima2  30999  ordtconnlem1  31870  measvuni  32178  measinb  32185  cndprobnul  32400  ballotlemfp1  32454  ballotlemgun  32487  chtvalz  32605  mrsubvrs  33480  mblfinlem2  35811  ntrkbimka  41618  neicvgbex  41692  limsup0  43206  subsalsal  43869  nnfoctbdjlem  43964