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 1542  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  fresaun  6705  fmpox  8013  fmpo  8014  tposf  8197  issmo  8281  axdc3lem4  10366  cardf  10463  smobeth  10500  seqf2  13974  hashfxnn0  14290  snopiswrd  14476  iswrddm0  14491  s1dm  14562  s2dm  14843  s7f1o  14919  ntrivcvgtail  15856  vdwlem8  16950  0ram  16982  gsumws1  18797  ga0  19264  efgsp1  19703  efgsfo  19705  efgredleme  19709  efgred  19714  ablfaclem2  20054  islinds2  21803  rhmply1vsca  22363  pmatcollpw3fi1lem1  22761  0met  24341  dvef  25957  dvfsumrlim2  26009  dchrisum0  27497  noxp1o  27641  trgcgrg  28597  tgcgr4  28613  axlowdimlem4  29028  uhgr0e  29154  vtxdumgrval  29570  wlkp1  29763  pthdlem2  29851  0wlk  30201  0spth  30211  0clwlkv  30216  wlk2v2e  30242  wlkl0  30452  padct  32806  wrdpmtrlast  33169  mbfmcnt  34428  coinfliprv  34643  matunitlindf  37953  fdc  38080  grposnOLD  38217  rabren3dioph  43261  amgm2d  44643  amgm3d  44644  fourierdlem80  46632  sge0iun  46865  0ome  46975  issmflem  47173  2ffzoeq  47788  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  line2x  49242  line2y  49243  amgmw2d  50291