Theorem feq2i 6694

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⟶wf 6529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-fn 6536  df-f 6537

This theorem is used by:  fresaun  6746  fmpox  8064  fmpo  8065  tposf  8252  issmo  8337  axdc3lem4  10455  cardf  10558  smobeth  10595  seqf2  14085  hashfxnn0  14401  snopiswrd  14588  iswrddm0  14603  s1dm  14675  s2dm  14961  s7f1o  15039  ntrivcvgtail  15989  vdwlem8  17080  0ram  17112  gsumws1  18947  ga0  19425  efgsp1  19864  efgsfo  19866  efgredleme  19870  efgred  19875  ablfaclem2  20215  islinds2  22026  rhmply1vsca  22610  matunitlindf  22903  pmatcollpw3fi1lem1  23011  0met  24592  dvef  26207  dvfsumrlim2  26259  dchrisum0  27756  noxp1o  27899  trgcgrg  28857  tgcgr4  28873  axlowdimlem4  29402  uhgr0e  29528  vtxdumgrval  29946  wlkp1  30139  pthdlem2  30233  0wlk  30586  0spth  30596  0clwlkv  30601  wlk2v2e  30637  wlkl0  30847  padct  33189  wrdpmtrlast  33533  mbfmcnt  34779  coinfliprv  34994  rankfo  35619  fdc  38495  grposnOLD  38632  rabren3dioph  43656  amgm2d  45038  amgm3d  45039  fourierdlem80  47014  sge0iun  47247  0ome  47357  issmflem  47555  2ffzoeq  48216  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  line2x  49684  line2y  49685  amgmw2d  50822