Theorem 0in 4360

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 4172	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4358	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2752	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1540   ∩ cin 3913  ∅c0 4296

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-in 3921  df-nul 4297

This theorem is referenced by:  pred0  6308  fresaunres2  6732  fnsuppeq0  8171  setsfun  17141  setsfun0  17142  indistopon  22888  fctop  22891  cctop  22893  restsn  23057  filconn  23770  chtdif  27068  ppidif  27073  ppi1  27074  cht1  27075  0res  32532  ofpreima2  32590  ordtconnlem1  33914  measvuni  34204  measinb  34211  cndprobnul  34428  ballotlemfp1  34483  ballotlemgun  34516  chtvalz  34620  mrsubvrs  35509  mblfinlem2  37652  ntrkbimka  44027  neicvgbex  44101  limsup0  45692  subsalsal  46357  nnfoctbdjlem  46453  setc1onsubc  49591