Theorem 0in 4348

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		in0 4346	. 2 ⊢ (𝐴 ∩ ∅) = ∅
2	1	ineqcomi 4161	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1559   ∩ cin 3901  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-in 3909  df-nul 4284

This theorem is referenced by:  pred0  6316  fresaunres2  6730  fnsuppeq0  8165  setsfun  17197  setsfun0  17198  indistopon  23048  fctop  23051  cctop  23053  restsn  23217  filconn  23930  chtdif  27209  ppidif  27214  ppi1  27215  cht1  27216  0res  32762  ofpreima2  32828  ordtconnlem1  34181  measvuni  34471  measinb  34478  cndprobnul  34694  ballotlemfp1  34749  ballotlemgun  34782  chtvalz  34883  mrsubvrs  35832  mblfinlem2  38117  ntrkbimka  44574  neicvgbex  44648  limsup0  46228  subsalsal  46893  nnfoctbdjlem  46989  setc1onsubc  50183