Theorem feq2i 6708

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

Syntax hints:   ↔ wb 206   = wceq 1539  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-fn 6544  df-f 6545

This theorem is referenced by:  fresaun  6759  fmpox  8074  fmpo  8075  tposf  8261  issmo  8370  axdc3lem4  10475  cardf  10572  smobeth  10608  seqf2  14044  hashfxnn0  14358  snopiswrd  14543  iswrddm0  14558  s1dm  14628  s2dm  14911  s7f1o  14987  ntrivcvgtail  15918  vdwlem8  17008  0ram  17040  gsumws1  18820  ga0  19285  efgsp1  19723  efgsfo  19725  efgredleme  19729  efgred  19734  ablfaclem2  20074  islinds2  21787  rhmply1vsca  22340  pmatcollpw3fi1lem1  22740  0met  24321  dvef  25954  dvfsumrlim2  26009  dchrisum0  27500  noxp1o  27644  trgcgrg  28459  tgcgr4  28475  axlowdimlem4  28890  uhgr0e  29016  vtxdumgrval  29432  wlkp1  29627  pthdlem2  29716  0wlk  30063  0spth  30073  0clwlkv  30078  wlk2v2e  30104  wlkl0  30314  padct  32666  wrdpmtrlast  33052  mbfmcnt  34229  coinfliprv  34444  matunitlindf  37584  fdc  37711  grposnOLD  37848  rabren3dioph  42789  amgm2d  44173  amgm3d  44174  fourierdlem80  46158  sge0iun  46391  0ome  46501  issmflem  46699  2ffzoeq  47297  nnsum4primesodd  47741  nnsum4primesoddALTV  47742  nnsum4primeseven  47745  nnsum4primesevenALTV  47746  line2x  48633  line2y  48634  amgmw2d  49331