Theorem 0in 4363

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

Syntax hints:   = wceq 1540   ∩ cin 3916  ∅c0 4299

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-in 3924  df-nul 4300

This theorem is referenced by:  pred0  6311  fresaunres2  6735  fnsuppeq0  8174  setsfun  17148  setsfun0  17149  indistopon  22895  fctop  22898  cctop  22900  restsn  23064  filconn  23777  chtdif  27075  ppidif  27080  ppi1  27081  cht1  27082  0res  32539  ofpreima2  32597  ordtconnlem1  33921  measvuni  34211  measinb  34218  cndprobnul  34435  ballotlemfp1  34490  ballotlemgun  34523  chtvalz  34627  mrsubvrs  35516  mblfinlem2  37659  ntrkbimka  44034  neicvgbex  44108  limsup0  45699  subsalsal  46364  nnfoctbdjlem  46460  setc1onsubc  49595