Theorem feq2i 6650

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-fn 6491  df-f 6492

This theorem is referenced by:  fresaun  6701  fmpox  8007  fmpo  8008  tposf  8192  issmo  8276  axdc3lem4  10353  cardf  10450  smobeth  10486  seqf2  13932  hashfxnn0  14248  snopiswrd  14434  iswrddm0  14449  s1dm  14520  s2dm  14801  s7f1o  14877  ntrivcvgtail  15811  vdwlem8  16904  0ram  16936  gsumws1  18750  ga0  19214  efgsp1  19653  efgsfo  19655  efgredleme  19659  efgred  19664  ablfaclem2  20004  islinds2  21754  rhmply1vsca  22306  pmatcollpw3fi1lem1  22704  0met  24284  dvef  25914  dvfsumrlim2  25969  dchrisum0  27461  noxp1o  27605  trgcgrg  28496  tgcgr4  28512  axlowdimlem4  28927  uhgr0e  29053  vtxdumgrval  29469  wlkp1  29662  pthdlem2  29750  0wlk  30100  0spth  30110  0clwlkv  30115  wlk2v2e  30141  wlkl0  30351  padct  32707  wrdpmtrlast  33071  mbfmcnt  34304  coinfliprv  34519  matunitlindf  37681  fdc  37808  grposnOLD  37945  rabren3dioph  42935  amgm2d  44318  amgm3d  44319  fourierdlem80  46311  sge0iun  46544  0ome  46654  issmflem  46852  2ffzoeq  47454  nnsum4primesodd  47923  nnsum4primesoddALTV  47924  nnsum4primeseven  47927  nnsum4primesevenALTV  47928  line2x  48882  line2y  48883  amgmw2d  49932