Theorem 0in 4332

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

Syntax hints:   = wceq 1547   ∩ cin 3889  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-in 3897  df-nul 4269

This theorem is referenced by:  pred0  6293  fresaunres2  6706  fnsuppeq0  8139  setsfun  17139  setsfun0  17140  indistopon  22991  fctop  22994  cctop  22996  restsn  23160  filconn  23873  chtdif  27146  ppidif  27151  ppi1  27152  cht1  27153  0res  32699  ofpreima2  32765  ordtconnlem1  34115  measvuni  34405  measinb  34412  cndprobnul  34628  ballotlemfp1  34683  ballotlemgun  34716  chtvalz  34820  mrsubvrs  35757  mblfinlem2  38032  ntrkbimka  44489  neicvgbex  44563  limsup0  46144  subsalsal  46809  nnfoctbdjlem  46905  setc1onsubc  50099