Theorem feq2i 6654

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 6641	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Syntax hints:   ↔ wb 206   = wceq 1541  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-fn 6495  df-f 6496

This theorem is referenced by:  fresaun  6705  fmpox  8011  fmpo  8012  tposf  8196  issmo  8280  axdc3lem4  10363  cardf  10460  smobeth  10497  seqf2  13944  hashfxnn0  14260  snopiswrd  14446  iswrddm0  14461  s1dm  14532  s2dm  14813  s7f1o  14889  ntrivcvgtail  15823  vdwlem8  16916  0ram  16948  gsumws1  18763  ga0  19227  efgsp1  19666  efgsfo  19668  efgredleme  19672  efgred  19677  ablfaclem2  20017  islinds2  21768  rhmply1vsca  22332  pmatcollpw3fi1lem1  22730  0met  24310  dvef  25940  dvfsumrlim2  25995  dchrisum0  27487  noxp1o  27631  trgcgrg  28587  tgcgr4  28603  axlowdimlem4  29018  uhgr0e  29144  vtxdumgrval  29560  wlkp1  29753  pthdlem2  29841  0wlk  30191  0spth  30201  0clwlkv  30206  wlk2v2e  30232  wlkl0  30442  padct  32797  wrdpmtrlast  33175  mbfmcnt  34425  coinfliprv  34640  matunitlindf  37819  fdc  37946  grposnOLD  38083  rabren3dioph  43057  amgm2d  44439  amgm3d  44440  fourierdlem80  46430  sge0iun  46663  0ome  46773  issmflem  46971  2ffzoeq  47573  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  line2x  49000  line2y  49001  amgmw2d  50049