Theorem 0in 4350

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

Assertion

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

Proof of Theorem 0in

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3901  ∅c0 4282

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-in 3909  df-nul 4283

This theorem is used by:  pred0  6337  fresaunres2  6751  fnsuppeq0  8194  setsfun  17269  setsfun0  17270  indistopon  23232  fctop  23235  cctop  23237  restsn  23401  filconn  24115  chtdif  27402  ppidif  27407  ppi1  27408  cht1  27409  0res  33084  ofpreima2  33147  ordtconnlem1  34442  measvuni  34733  measinb  34740  cndprobnul  34956  ballotlemfp1  35011  ballotlemgun  35044  chtvalz  35145  mrsubvrs  36109  mblfinlem2  38415  ntrkbimka  44886  neicvgbex  44960  limsup0  46530  subsalsal  47195  nnfoctbdjlem  47291  setc1onsubc  50536