Theorem 0in 4397

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 4209	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4395	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2765	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1540   ∩ cin 3950  ∅c0 4333

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958  df-nul 4334

This theorem is referenced by:  pred0  6356  fresaunres2  6780  fnsuppeq0  8217  setsfun  17208  setsfun0  17209  indistopon  23008  fctop  23011  cctop  23013  restsn  23178  filconn  23891  chtdif  27201  ppidif  27206  ppi1  27207  cht1  27208  0res  32616  ofpreima2  32676  ordtconnlem1  33923  measvuni  34215  measinb  34222  cndprobnul  34439  ballotlemfp1  34494  ballotlemgun  34527  chtvalz  34644  mrsubvrs  35527  mblfinlem2  37665  ntrkbimka  44051  neicvgbex  44125  limsup0  45709  subsalsal  46374  nnfoctbdjlem  46470