Theorem feq2i 6704

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-fn 6546  df-f 6547

This theorem is used by:  fresaun  6756  fmpox  8073  fmpo  8074  tposf  8259  issmo  8344  axdc3lem4  10455  cardf  10552  smobeth  10589  seqf2  14077  hashfxnn0  14393  snopiswrd  14580  iswrddm0  14595  s1dm  14667  s2dm  14953  s7f1o  15029  ntrivcvgtail  15980  vdwlem8  17073  0ram  17105  gsumws1  18928  ga0  19399  efgsp1  19838  efgsfo  19840  efgredleme  19844  efgred  19849  ablfaclem2  20189  islinds2  22000  rhmply1vsca  22582  pmatcollpw3fi1lem1  22980  0met  24560  dvef  26176  dvfsumrlim2  26228  dchrisum0  27721  noxp1o  27864  trgcgrg  28821  tgcgr4  28837  axlowdimlem4  29332  uhgr0e  29458  vtxdumgrval  29873  wlkp1  30066  pthdlem2  30154  0wlk  30504  0spth  30514  0clwlkv  30519  wlk2v2e  30545  wlkl0  30755  padct  33100  wrdpmtrlast  33444  mbfmcnt  34690  coinfliprv  34905  rankfo  35530  matunitlindf  38310  fdc  38437  grposnOLD  38574  rabren3dioph  43583  amgm2d  44965  amgm3d  44966  fourierdlem80  46941  sge0iun  47174  0ome  47284  issmflem  47482  2ffzoeq  48106  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  line2x  49575  line2y  49576  amgmw2d  50693