Theorem 0in 4347

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

Assertion

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

Proof of Theorem 0in

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

This proof depends on syntax axioms:   = wceq 1570   ∩ cin 3898  ∅c0 4279

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-nul 4280

This theorem is used by:  pred0  6331  fresaunres2  6746  fnsuppeq0  8193  setsfun  17329  setsfun0  17330  indistopon  23299  fctop  23302  cctop  23304  restsn  23468  filconn  24182  chtdif  27467  ppidif  27472  ppi1  27473  cht1  27474  0res  33179  ofpreima2  33242  ordtconnlem1  34538  measvuni  34829  measinb  34836  cndprobnul  35052  ballotlemfp1  35107  ballotlemgun  35140  chtvalz  35241  mrsubvrs  36256  mblfinlem2  38544  ntrkbimka  44997  neicvgbex  45071  limsup0  46648  subsalsal  47313  nnfoctbdjlem  47409  setc1onsubc  50654