Theorem 0in 4357

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

Assertion

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

Proof of Theorem 0in

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3907  ∅c0 4289

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-in 3915  df-nul 4290

This theorem is used by:  pred0  6343  fresaunres2  6757  fnsuppeq0  8197  setsfun  17256  setsfun0  17257  indistopon  23195  fctop  23198  cctop  23200  restsn  23364  filconn  24077  chtdif  27359  ppidif  27364  ppi1  27365  cht1  27366  0res  32985  ofpreima2  33048  ordtconnlem1  34345  measvuni  34636  measinb  34643  cndprobnul  34859  ballotlemfp1  34914  ballotlemgun  34947  chtvalz  35048  mrsubvrs  36035  mblfinlem2  38350  ntrkbimka  44805  neicvgbex  44879  limsup0  46449  subsalsal  47114  nnfoctbdjlem  47210  setc1onsubc  50421