Theorem 0in 4195

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 4028	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4194	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2802	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1601   ∩ cin 3791  ∅c0 4141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-dif 3795  df-in 3799  df-nul 4142

This theorem is referenced by:  pred0  5963  fresaunres2  6326  fnsuppeq0  7605  setsfun  16290  setsfun0  16291  indistopon  21213  fctop  21216  cctop  21218  restsn  21382  filconn  22095  chtdif  25336  ppidif  25341  ppi1  25342  cht1  25343  ofpreima2  30031  ordtconnlem1  30568  measvuni  30875  measinb  30882  cndprobnul  31098  ballotlemfp1  31152  ballotlemgun  31185  chtvalz  31309  mrsubvrs  32018  mblfinlem2  34073  ntrkbimka  39292  limsup0  40834  subsalsal  41501  nnfoctbdjlem  41596