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 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-fn 6495  df-f 6496

This theorem is referenced by:  fresaun  6705  fmpox  8016  fmpo  8017  tposf  8201  issmo  8285  axdc3lem4  10373  cardf  10470  smobeth  10507  seqf2  13981  hashfxnn0  14297  snopiswrd  14483  iswrddm0  14498  s1dm  14569  s2dm  14850  s7f1o  14926  ntrivcvgtail  15863  vdwlem8  16957  0ram  16989  gsumws1  18804  ga0  19271  efgsp1  19710  efgsfo  19712  efgredleme  19716  efgred  19721  ablfaclem2  20061  islinds2  21795  rhmply1vsca  22378  pmatcollpw3fi1lem1  22776  0met  24356  dvef  25972  dvfsumrlim2  26024  dchrisum0  27508  noxp1o  27652  trgcgrg  28608  tgcgr4  28624  axlowdimlem4  29039  uhgr0e  29165  vtxdumgrval  29580  wlkp1  29773  pthdlem2  29861  0wlk  30211  0spth  30221  0clwlkv  30226  wlk2v2e  30252  wlkl0  30462  padct  32817  wrdpmtrlast  33181  mbfmcnt  34459  coinfliprv  34674  matunitlindf  37992  fdc  38119  grposnOLD  38256  rabren3dioph  43267  amgm2d  44649  amgm3d  44650  fourierdlem80  46636  sge0iun  46869  0ome  46979  issmflem  47177  2ffzoeq  47798  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  line2x  49252  line2y  49253  amgmw2d  50301