Theorem feq2i 6515

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

Syntax hints:   ↔ wb 209   = wceq 1543  ⟶wf 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-fn 6361  df-f 6362

This theorem is referenced by:  fco3OLD  6557  fresaun  6568  fmpox  7815  fmpo  7816  tposf  7974  issmo  8063  axdc3lem4  10032  cardf  10129  smobeth  10165  seqf2  13560  hashfxnn0  13868  snopiswrd  14043  iswrddm0  14058  s1dm  14130  s2dm  14420  ntrivcvgtail  15427  vdwlem8  16504  0ram  16536  gsumws1  18218  ga0  18646  efgsp1  19081  efgsfo  19083  efgredleme  19087  efgred  19092  ablfaclem2  19427  islinds2  20729  pmatcollpw3fi1lem1  21637  0met  23218  dvef  24831  dvfsumrlim2  24883  dchrisum0  26355  trgcgrg  26560  tgcgr4  26576  axlowdimlem4  26990  uhgr0e  27116  vtxdumgrval  27528  wlkp1  27723  pthdlem2  27809  0wlk  28153  0spth  28163  0clwlkv  28168  wlk2v2e  28194  wlkl0  28404  padct  30728  mbfmcnt  31901  coinfliprv  32115  noxp1o  33552  matunitlindf  35461  fdc  35589  grposnOLD  35726  rabren3dioph  40281  amgm2d  41428  amgm3d  41429  fourierdlem80  43345  sge0iun  43575  0ome  43685  issmflem  43878  2ffzoeq  44436  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  line2x  45716  line2y  45717  amgmw2d  46122