Theorem 0in 4324

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 4131	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4322	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2766	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1539   ∩ cin 3882  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-in 3890  df-nul 4254

This theorem is referenced by:  pred0  6227  fresaunres2  6630  fnsuppeq0  7979  setsfun  16800  setsfun0  16801  indistopon  22059  fctop  22062  cctop  22064  restsn  22229  filconn  22942  chtdif  26212  ppidif  26217  ppi1  26218  cht1  26219  0res  30844  ofpreima2  30905  ordtconnlem1  31776  measvuni  32082  measinb  32089  cndprobnul  32304  ballotlemfp1  32358  ballotlemgun  32391  chtvalz  32509  mrsubvrs  33384  mblfinlem2  35742  ntrkbimka  41537  neicvgbex  41611  limsup0  43125  subsalsal  43788  nnfoctbdjlem  43883