Theorem inteqd 4843

Description: Equality deduction for class intersection. (Contributed by NM, 2-Sep-2003.)

Hypothesis

Ref	Expression
inteqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
inteqd	⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Proof of Theorem inteqd

Step	Hyp	Ref	Expression
1		inteqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		inteq 4841	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1538  ∩ cint 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-int 4839

This theorem is referenced by:  intprg  4872  elreldm  5769  ordintdif  6208  fniinfv  6717  onsucmin  7516  elxp5  7610  1stval2  7688  2ndval2  7689  fundmen  8566  xpsnen  8584  unblem2  8755  unblem3  8756  fiint  8779  elfi2  8862  fi0  8868  elfiun  8878  tcvalg  9164  tz9.12lem3  9202  rankvalb  9210  rankvalg  9230  ranksnb  9240  rankonidlem  9241  cardval3  9365  cardidm  9372  harsucnn  9411  cfval  9658  cflim3  9673  coftr  9684  isfin3ds  9740  fin23lem17  9749  fin23lem39  9761  isf33lem  9777  isf34lem5  9789  isf34lem6  9791  wuncval  10153  tskmval  10250  cleq1  14334  dfrtrcl2  14413  mrcfval  16871  mrcval  16873  cycsubg2  18345  efgval  18835  lspfval  19738  lspval  19740  lsppropd  19783  aspval  20559  aspval2  20584  clsfval  21630  clsval  21642  clsval2  21655  hauscmplem  22011  cmpfi  22013  1stcfb  22050  fclscmp  22635  spanval  29116  chsupid  29195  intimafv  30470  zarclsint  31225  zarcmplem  31234  sigagenval  31509  kur14  32576  mclsval  32923  scutval  33378  igenval  35499  pclfvalN  37185  pclvalN  37186  diaintclN  38354  docaffvalN  38417  docafvalN  38418  docavalN  38419  dibintclN  38463  dihglb2  38638  dihintcl  38640  mzpval  39673  dnnumch3lem  39990  aomclem8  40005  rgspnval  40112  iotain  41121  salgenval  42963