Theorem 0in 4350

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

Syntax hints:   = wceq 1540   ∩ cin 3904  ∅c0 4286

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 3397  df-v 3440  df-dif 3908  df-in 3912  df-nul 4287

This theorem is referenced by:  pred0  6287  fresaunres2  6700  fnsuppeq0  8132  setsfun  17100  setsfun0  17101  indistopon  22904  fctop  22907  cctop  22909  restsn  23073  filconn  23786  chtdif  27084  ppidif  27089  ppi1  27090  cht1  27091  0res  32565  ofpreima2  32623  ordtconnlem1  33893  measvuni  34183  measinb  34190  cndprobnul  34407  ballotlemfp1  34462  ballotlemgun  34495  chtvalz  34599  mrsubvrs  35497  mblfinlem2  37640  ntrkbimka  44014  neicvgbex  44088  limsup0  45679  subsalsal  46344  nnfoctbdjlem  46440  setc1onsubc  49591