Theorem 0in 4420

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 4230	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4418	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2768	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1537   ∩ cin 3975  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-in 3983  df-nul 4353

This theorem is referenced by:  pred0  6367  fresaunres2  6793  fnsuppeq0  8233  setsfun  17218  setsfun0  17219  indistopon  23029  fctop  23032  cctop  23034  restsn  23199  filconn  23912  chtdif  27219  ppidif  27224  ppi1  27225  cht1  27226  0res  32625  ofpreima2  32684  ordtconnlem1  33870  measvuni  34178  measinb  34185  cndprobnul  34402  ballotlemfp1  34456  ballotlemgun  34489  chtvalz  34606  mrsubvrs  35490  mblfinlem2  37618  ntrkbimka  44000  neicvgbex  44074  limsup0  45615  subsalsal  46280  nnfoctbdjlem  46376