Theorem inteqd 4873

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 4871	. 2 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → ∩ 𝐴 = ∩ 𝐵)

Syntax hints:   → wi 4   = wceq 1533  ∩ cint 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-int 4869

This theorem is referenced by:  intprg  4902  elreldm  5799  ordintdif  6234  fniinfv  6736  onsucmin  7530  elxp5  7622  1stval2  7700  2ndval2  7701  fundmen  8577  xpsnen  8595  unblem2  8765  unblem3  8766  fiint  8789  elfi2  8872  fi0  8878  elfiun  8888  tcvalg  9174  tz9.12lem3  9212  rankvalb  9220  rankvalg  9240  ranksnb  9250  rankonidlem  9251  cardval3  9375  cardidm  9382  cfval  9663  cflim3  9678  coftr  9689  isfin3ds  9745  fin23lem17  9754  fin23lem39  9766  isf33lem  9782  isf34lem5  9794  isf34lem6  9796  wuncval  10158  tskmval  10255  cleq1  14337  dfrtrcl2  14415  mrcfval  16873  mrcval  16875  cycsubg2  18347  efgval  18837  lspfval  19739  lspval  19741  lsppropd  19784  aspval  20096  aspval2  20121  clsfval  21627  clsval  21639  clsval2  21652  hauscmplem  22008  cmpfi  22010  1stcfb  22047  fclscmp  22632  spanval  29104  chsupid  29183  sigagenval  31394  kur14  32458  mclsval  32805  scutval  33260  igenval  35333  pclfvalN  37019  pclvalN  37020  diaintclN  38188  docaffvalN  38251  docafvalN  38252  docavalN  38253  dibintclN  38297  dihglb2  38472  dihintcl  38474  mzpval  39322  dnnumch3lem  39639  aomclem8  39654  rgspnval  39761  harsucnn  39896  iotain  40742  salgenval  42600