Theorem feq2i 6699

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

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

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 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-fn 6540  df-f 6541

This theorem is used by:  fresaun  6751  fmpox  8076  fmpo  8077  tposf  8264  issmo  8349  axdc3lem4  10524  cardf  10627  smobeth  10664  seqf2  14157  hashfxnn0  14474  snopiswrd  14661  iswrddm0  14676  s1dm  14748  s2dm  15034  s7f1o  15112  ntrivcvgtail  16062  vdwlem8  17159  0ram  17191  gsumws1  19027  ga0  19505  efgsp1  19944  efgsfo  19946  efgredleme  19950  efgred  19955  ablfaclem2  20295  islinds2  22112  rhmply1vsca  22696  matunitlindf  22989  pmatcollpw3fi1lem1  23097  0met  24678  dvef  26293  dvfsumrlim2  26345  dchrisum0  27840  noxp1o  28013  trgcgrg  28971  tgcgr4  28987  axlowdimlem4  29516  uhgr0e  29642  vtxdumgrval  30060  wlkp1  30253  pthdlem2  30347  0wlk  30700  0spth  30710  0clwlkv  30715  wlk2v2e  30751  wlkl0  30961  padct  33303  wrdpmtrlast  33647  mbfmcnt  34893  coinfliprv  35108  rankfo  35724  fdc  38659  grposnOLD  38796  rabren3dioph  43801  amgm2d  45183  amgm3d  45184  fourierdlem80  47165  sge0iun  47398  0ome  47508  issmflem  47706  2ffzoeq  48367  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  line2x  49835  line2y  49836  amgmw2d  50958