Theorem feq2i 6648

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

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

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 6489  df-f 6490

This theorem is referenced by:  fresaun  6699  fmpox  8009  fmpo  8010  tposf  8194  issmo  8278  axdc3lem4  10366  cardf  10463  smobeth  10499  seqf2  13946  hashfxnn0  14262  snopiswrd  14448  iswrddm0  14463  s1dm  14533  s2dm  14815  s7f1o  14891  ntrivcvgtail  15825  vdwlem8  16918  0ram  16950  gsumws1  18730  ga0  19195  efgsp1  19634  efgsfo  19636  efgredleme  19640  efgred  19645  ablfaclem2  19985  islinds2  21738  rhmply1vsca  22291  pmatcollpw3fi1lem1  22689  0met  24270  dvef  25900  dvfsumrlim2  25955  dchrisum0  27447  noxp1o  27591  trgcgrg  28478  tgcgr4  28494  axlowdimlem4  28908  uhgr0e  29034  vtxdumgrval  29450  wlkp1  29643  pthdlem2  29731  0wlk  30078  0spth  30088  0clwlkv  30093  wlk2v2e  30119  wlkl0  30329  padct  32676  wrdpmtrlast  33048  mbfmcnt  34238  coinfliprv  34453  matunitlindf  37600  fdc  37727  grposnOLD  37864  rabren3dioph  42791  amgm2d  44174  amgm3d  44175  fourierdlem80  46171  sge0iun  46404  0ome  46514  issmflem  46712  2ffzoeq  47315  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  line2x  48743  line2y  48744  amgmw2d  49793