Theorem 0in 4301

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 4128	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4299	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2821	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1538   ∩ cin 3880  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-dif 3884  df-in 3888  df-nul 4244

This theorem is referenced by:  pred0  6146  fresaunres2  6524  fnsuppeq0  7841  setsfun  16510  setsfun0  16511  indistopon  21606  fctop  21609  cctop  21611  restsn  21775  filconn  22488  chtdif  25743  ppidif  25748  ppi1  25749  cht1  25750  0res  30367  ofpreima2  30429  ordtconnlem1  31277  measvuni  31583  measinb  31590  cndprobnul  31805  ballotlemfp1  31859  ballotlemgun  31892  chtvalz  32010  mrsubvrs  32882  mblfinlem2  35095  ntrkbimka  40741  neicvgbex  40815  limsup0  42336  subsalsal  42999  nnfoctbdjlem  43094