Theorem feq2i 6707

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 205   = wceq 1542  ⟶wf 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6544  df-f 6545

This theorem is referenced by:  fco3OLD  6749  fresaun  6760  fmpox  8050  fmpo  8051  tposf  8236  issmo  8345  axdc3lem4  10445  cardf  10542  smobeth  10578  seqf2  13984  hashfxnn0  14294  snopiswrd  14470  iswrddm0  14485  s1dm  14555  s2dm  14838  ntrivcvgtail  15843  vdwlem8  16918  0ram  16950  gsumws1  18716  ga0  19157  efgsp1  19600  efgsfo  19602  efgredleme  19606  efgred  19611  ablfaclem2  19951  islinds2  21360  pmatcollpw3fi1lem1  22280  0met  23864  dvef  25489  dvfsumrlim2  25541  dchrisum0  27013  noxp1o  27156  trgcgrg  27756  tgcgr4  27772  axlowdimlem4  28193  uhgr0e  28321  vtxdumgrval  28733  wlkp1  28928  pthdlem2  29015  0wlk  29359  0spth  29369  0clwlkv  29374  wlk2v2e  29400  wlkl0  29610  padct  31932  mbfmcnt  33256  coinfliprv  33470  matunitlindf  36475  fdc  36602  grposnOLD  36739  rabren3dioph  41539  amgm2d  42936  amgm3d  42937  fourierdlem80  44889  sge0iun  45122  0ome  45232  issmflem  45430  2ffzoeq  46023  nnsum4primesodd  46451  nnsum4primesoddALTV  46452  nnsum4primeseven  46455  nnsum4primesevenALTV  46456  line2x  47394  line2y  47395  amgmw2d  47805