Theorem feq2i 6680

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514  df-f 6515

This theorem is referenced by:  fresaun  6731  fmpox  8046  fmpo  8047  tposf  8233  issmo  8317  axdc3lem4  10406  cardf  10503  smobeth  10539  seqf2  13986  hashfxnn0  14302  snopiswrd  14488  iswrddm0  14503  s1dm  14573  s2dm  14856  s7f1o  14932  ntrivcvgtail  15866  vdwlem8  16959  0ram  16991  gsumws1  18765  ga0  19230  efgsp1  19667  efgsfo  19669  efgredleme  19673  efgred  19678  ablfaclem2  20018  islinds2  21722  rhmply1vsca  22275  pmatcollpw3fi1lem1  22673  0met  24254  dvef  25884  dvfsumrlim2  25939  dchrisum0  27431  noxp1o  27575  trgcgrg  28442  tgcgr4  28458  axlowdimlem4  28872  uhgr0e  28998  vtxdumgrval  29414  wlkp1  29609  pthdlem2  29698  0wlk  30045  0spth  30055  0clwlkv  30060  wlk2v2e  30086  wlkl0  30296  padct  32643  wrdpmtrlast  33050  mbfmcnt  34259  coinfliprv  34474  matunitlindf  37612  fdc  37739  grposnOLD  37876  rabren3dioph  42803  amgm2d  44187  amgm3d  44188  fourierdlem80  46184  sge0iun  46417  0ome  46527  issmflem  46725  2ffzoeq  47328  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  line2x  48743  line2y  48744  amgmw2d  49793