Theorem 0in 4395

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 4199	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4393	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2753	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1533   ∩ cin 3943  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-in 3951  df-nul 4323

This theorem is referenced by:  pred0  6343  fresaunres2  6769  fnsuppeq0  8197  setsfun  17143  setsfun0  17144  indistopon  22948  fctop  22951  cctop  22953  restsn  23118  filconn  23831  chtdif  27135  ppidif  27140  ppi1  27141  cht1  27142  0res  32472  ofpreima2  32533  ordtconnlem1  33656  measvuni  33964  measinb  33971  cndprobnul  34188  ballotlemfp1  34242  ballotlemgun  34275  chtvalz  34392  mrsubvrs  35263  mblfinlem2  37262  ntrkbimka  43610  neicvgbex  43684  limsup0  45220  subsalsal  45885  nnfoctbdjlem  45981