Theorem 0in 4338

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

Syntax hints:   = wceq 1542   ∩ cin 3889  ∅c0 4274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275

This theorem is referenced by:  pred0  6293  fresaunres2  6706  fnsuppeq0  8135  setsfun  17132  setsfun0  17133  indistopon  22976  fctop  22979  cctop  22981  restsn  23145  filconn  23858  chtdif  27135  ppidif  27140  ppi1  27141  cht1  27142  0res  32688  ofpreima2  32754  ordtconnlem1  34084  measvuni  34374  measinb  34381  cndprobnul  34597  ballotlemfp1  34652  ballotlemgun  34685  chtvalz  34789  mrsubvrs  35720  mblfinlem2  37993  ntrkbimka  44483  neicvgbex  44557  limsup0  46140  subsalsal  46805  nnfoctbdjlem  46901  setc1onsubc  50089