Theorem feq2i 6576

Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)

Hypothesis

Ref	Expression
feq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
feq2i	⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Proof of Theorem feq2i

Step	Hyp	Ref	Expression
1		feq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		feq2 6566	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Syntax hints:   ↔ wb 205   = wceq 1539  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421  df-f 6422

This theorem is referenced by:  fco3OLD  6618  fresaun  6629  fmpox  7880  fmpo  7881  tposf  8041  issmo  8150  axdc3lem4  10140  cardf  10237  smobeth  10273  seqf2  13670  hashfxnn0  13979  snopiswrd  14154  iswrddm0  14169  s1dm  14241  s2dm  14531  ntrivcvgtail  15540  vdwlem8  16617  0ram  16649  gsumws1  18391  ga0  18819  efgsp1  19258  efgsfo  19260  efgredleme  19264  efgred  19269  ablfaclem2  19604  islinds2  20930  pmatcollpw3fi1lem1  21843  0met  23427  dvef  25049  dvfsumrlim2  25101  dchrisum0  26573  trgcgrg  26780  tgcgr4  26796  axlowdimlem4  27216  uhgr0e  27344  vtxdumgrval  27756  wlkp1  27951  pthdlem2  28037  0wlk  28381  0spth  28391  0clwlkv  28396  wlk2v2e  28422  wlkl0  28632  padct  30956  mbfmcnt  32135  coinfliprv  32349  noxp1o  33793  matunitlindf  35702  fdc  35830  grposnOLD  35967  rabren3dioph  40553  amgm2d  41698  amgm3d  41699  fourierdlem80  43617  sge0iun  43847  0ome  43957  issmflem  44150  2ffzoeq  44708  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  line2x  45988  line2y  45989  amgmw2d  46394