Theorem 0in 4394

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 4202	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4392	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2758	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1539   ∩ cin 3948  ∅c0 4323

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3952  df-in 3956  df-nul 4324

This theorem is referenced by:  pred0  6337  fresaunres2  6764  fnsuppeq0  8181  setsfun  17110  setsfun0  17111  indistopon  22726  fctop  22729  cctop  22731  restsn  22896  filconn  23609  chtdif  26896  ppidif  26901  ppi1  26902  cht1  26903  0res  32099  ofpreima2  32156  ordtconnlem1  33200  measvuni  33508  measinb  33515  cndprobnul  33732  ballotlemfp1  33786  ballotlemgun  33819  chtvalz  33937  mrsubvrs  34809  mblfinlem2  36831  ntrkbimka  43093  neicvgbex  43167  limsup0  44710  subsalsal  45375  nnfoctbdjlem  45471