Theorem 0in 4354

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 4352	. 2 ⊢ (𝐴 ∩ ∅) = ∅
2	1	ineqcomi 4166	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1563   ∩ cin 3906  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-in 3914  df-nul 4289

This theorem is referenced by:  pred0  6325  fresaunres2  6740  fnsuppeq0  8176  setsfun  17219  setsfun0  17220  indistopon  23115  fctop  23118  cctop  23120  restsn  23284  filconn  23997  chtdif  27276  ppidif  27281  ppi1  27282  cht1  27283  0res  32854  ofpreima2  32919  ordtconnlem1  34226  measvuni  34516  measinb  34523  cndprobnul  34739  ballotlemfp1  34794  ballotlemgun  34827  chtvalz  34928  mrsubvrs  35880  mblfinlem2  38164  ntrkbimka  44621  neicvgbex  44695  limsup0  46267  subsalsal  46932  nnfoctbdjlem  47028  setc1onsubc  50232