Theorem 0in 4002

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		incom 3838	. 2 ⊢ (∅ ∩ 𝐴) = (𝐴 ∩ ∅)
2		in0 4001	. 2 ⊢ (𝐴 ∩ ∅) = ∅
3	1, 2	eqtri 2673	1 ⊢ (∅ ∩ 𝐴) = ∅

Syntax hints:   = wceq 1523   ∩ cin 3606  ∅c0 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-nul 3949

This theorem is referenced by:  pred0  5748  fnsuppeq0  7368  setsfun  15940  setsfun0  15941  indistopon  20853  fctop  20856  cctop  20858  restsn  21022  filconn  21734  chtdif  24929  ppidif  24934  ppi1  24935  cht1  24936  ofpreima2  29594  ordtconnlem1  30098  measvuni  30405  measinb  30412  cndprobnul  30627  ballotlemfp1  30681  ballotlemgun  30714  chtvalz  30835  mrsubvrs  31545  mblfinlem2  33577  ntrkbimka  38653  limsup0  40244  subsalsal  40895  nnfoctbdjlem  40990