Theorem feq2i 6687

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

Syntax hints:   ↔ wb 209   = wceq 1563  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-fn 6528  df-f 6529

This theorem is referenced by:  fresaun  6739  fmpox  8052  fmpo  8053  tposf  8238  issmo  8323  axdc3lem4  10425  cardf  10522  smobeth  10559  seqf2  14045  hashfxnn0  14361  snopiswrd  14548  iswrddm0  14563  s1dm  14634  s2dm  14915  s7f1o  14991  ntrivcvgtail  15942  vdwlem8  17036  0ram  17068  gsumws1  18885  ga0  19356  efgsp1  19795  efgsfo  19797  efgredleme  19801  efgred  19806  ablfaclem2  20146  islinds2  21920  rhmply1vsca  22502  pmatcollpw3fi1lem1  22900  0met  24480  dvef  26096  dvfsumrlim2  26148  dchrisum0  27638  noxp1o  27781  trgcgrg  28738  tgcgr4  28754  axlowdimlem4  29200  uhgr0e  29326  vtxdumgrval  29741  wlkp1  29934  pthdlem2  30022  0wlk  30372  0spth  30382  0clwlkv  30387  wlk2v2e  30413  wlkl0  30623  padct  32971  wrdpmtrlast  33321  mbfmcnt  34570  coinfliprv  34785  matunitlindf  38124  fdc  38251  grposnOLD  38388  rabren3dioph  43399  amgm2d  44781  amgm3d  44782  fourierdlem80  46759  sge0iun  46992  0ome  47102  issmflem  47300  2ffzoeq  47921  nnsum4primesodd  48417  nnsum4primesoddALTV  48418  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  line2x  49386  line2y  49387  amgmw2d  50434