Theorem feq2i 6592

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

Syntax hints:   ↔ wb 205   = wceq 1539  ⟶wf 6429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fn 6436  df-f 6437

This theorem is referenced by:  fco3OLD  6634  fresaun  6645  fmpox  7907  fmpo  7908  tposf  8070  issmo  8179  axdc3lem4  10209  cardf  10306  smobeth  10342  seqf2  13742  hashfxnn0  14051  snopiswrd  14226  iswrddm0  14241  s1dm  14313  s2dm  14603  ntrivcvgtail  15612  vdwlem8  16689  0ram  16721  gsumws1  18476  ga0  18904  efgsp1  19343  efgsfo  19345  efgredleme  19349  efgred  19354  ablfaclem2  19689  islinds2  21020  pmatcollpw3fi1lem1  21935  0met  23519  dvef  25144  dvfsumrlim2  25196  dchrisum0  26668  trgcgrg  26876  tgcgr4  26892  axlowdimlem4  27313  uhgr0e  27441  vtxdumgrval  27853  wlkp1  28049  pthdlem2  28136  0wlk  28480  0spth  28490  0clwlkv  28495  wlk2v2e  28521  wlkl0  28731  padct  31054  mbfmcnt  32235  coinfliprv  32449  noxp1o  33866  matunitlindf  35775  fdc  35903  grposnOLD  36040  rabren3dioph  40637  amgm2d  41809  amgm3d  41810  fourierdlem80  43727  sge0iun  43957  0ome  44067  issmflem  44263  2ffzoeq  44820  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  line2x  46100  line2y  46101  amgmw2d  46508