Theorem 0in 4355

Description: The intersection of the empty set with a class is the empty set. Commuted form of 0in 4355. (Contributed by Glauco Siliprandi, 17-Aug-2020.)

Assertion

Ref	Expression
0in	⊢ (∅ ∩ 𝐴) = ∅

Proof of Theorem 0in

Step	Hyp	Ref	Expression
1		in0 4353	. 2 ⊢ (𝐴 ∩ ∅) = ∅
2	1	ineqcomi 4165	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1570   ∩ cin 3905  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-in 3913  df-nul 4288

This theorem is referenced by:  pred0  6338  fresaunres2  6752  fnsuppeq0  8189  setsfun  17232  setsfun0  17233  indistopon  23139  fctop  23142  cctop  23144  restsn  23308  filconn  24021  chtdif  27303  ppidif  27308  ppi1  27309  cht1  27310  0res  32929  ofpreima2  32992  ordtconnlem1  34295  measvuni  34585  measinb  34592  cndprobnul  34808  ballotlemfp1  34863  ballotlemgun  34896  chtvalz  34997  mrsubvrs  35995  mblfinlem2  38290  ntrkbimka  44747  neicvgbex  44821  limsup0  46391  subsalsal  47056  nnfoctbdjlem  47152  setc1onsubc  50363