Theorem feq2i 6588

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

Syntax hints:   ↔ wb 205   = wceq 1541  ⟶wf 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-fn 6433  df-f 6434

This theorem is referenced by:  fco3OLD  6630  fresaun  6641  fmpox  7893  fmpo  7894  tposf  8054  issmo  8163  axdc3lem4  10193  cardf  10290  smobeth  10326  seqf2  13723  hashfxnn0  14032  snopiswrd  14207  iswrddm0  14222  s1dm  14294  s2dm  14584  ntrivcvgtail  15593  vdwlem8  16670  0ram  16702  gsumws1  18457  ga0  18885  efgsp1  19324  efgsfo  19326  efgredleme  19330  efgred  19335  ablfaclem2  19670  islinds2  21001  pmatcollpw3fi1lem1  21916  0met  23500  dvef  25125  dvfsumrlim2  25177  dchrisum0  26649  trgcgrg  26857  tgcgr4  26873  axlowdimlem4  27294  uhgr0e  27422  vtxdumgrval  27834  wlkp1  28029  pthdlem2  28115  0wlk  28459  0spth  28469  0clwlkv  28474  wlk2v2e  28500  wlkl0  28710  padct  31033  mbfmcnt  32214  coinfliprv  32428  noxp1o  33845  matunitlindf  35754  fdc  35882  grposnOLD  36019  rabren3dioph  40617  amgm2d  41762  amgm3d  41763  fourierdlem80  43681  sge0iun  43911  0ome  44021  issmflem  44214  2ffzoeq  44772  nnsum4primesodd  45200  nnsum4primesoddALTV  45201  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  line2x  46052  line2y  46053  amgmw2d  46460