Theorem feq2i 6731

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-fn 6569  df-f 6570

This theorem is used by:  fresaun  6783  fmpox  8113  fmpo  8114  tposf  8309  issmo  8394  axdc3lem4  10570  cardf  10673  smobeth  10710  seqf2  14204  hashfxnn0  14522  snopiswrd  14709  iswrddm0  14724  s1dm  14796  s2dm  15083  s7f1o  15162  ntrivcvgtail  16113  vdwlem8  17210  0ram  17242  gsumws1  19084  ga0  19563  efgsp1  20002  efgsfo  20004  efgredleme  20008  efgred  20013  ablfaclem2  20353  islinds2  22174  rhmply1vsca  22758  matunitlindf  23051  pmatcollpw3fi1lem1  23159  0met  24740  dvef  26355  dvfsumrlim2  26407  dchrisum0  27904  noxp1o  28077  trgcgrg  29035  tgcgr4  29051  axlowdimlem4  29580  uhgr0e  29706  vtxdumgrval  30124  wlkp1  30317  pthdlem2  30411  0wlk  30764  0spth  30774  0clwlkv  30779  wlk2v2e  30815  wlkl0  31025  padct  33407  wrdpmtrlast  33753  mbfmcnt  35011  coinfliprv  35226  rankfo  35858  fdc  38945  grposnOLD  39082  rabren3dioph  44088  amgm2d  45459  amgm3d  45460  fourierdlem80  47469  sge0iun  47702  0ome  47812  issmflem  48010  2ffzoeq  48671  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  line2x  50197  line2y  50198  amgmw2d  51417