Theorem feq2i 6710

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

Syntax hints:   ↔ wb 205   = wceq 1542  ⟶wf 6540

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 6547  df-f 6548

This theorem is referenced by:  fco3OLD  6752  fresaun  6763  fmpox  8053  fmpo  8054  tposf  8239  issmo  8348  axdc3lem4  10448  cardf  10545  smobeth  10581  seqf2  13987  hashfxnn0  14297  snopiswrd  14473  iswrddm0  14488  s1dm  14558  s2dm  14841  ntrivcvgtail  15846  vdwlem8  16921  0ram  16953  gsumws1  18719  ga0  19162  efgsp1  19605  efgsfo  19607  efgredleme  19611  efgred  19616  ablfaclem2  19956  islinds2  21368  pmatcollpw3fi1lem1  22288  0met  23872  dvef  25497  dvfsumrlim2  25549  dchrisum0  27023  noxp1o  27166  trgcgrg  27766  tgcgr4  27782  axlowdimlem4  28203  uhgr0e  28331  vtxdumgrval  28743  wlkp1  28938  pthdlem2  29025  0wlk  29369  0spth  29379  0clwlkv  29384  wlk2v2e  29410  wlkl0  29620  padct  31944  mbfmcnt  33267  coinfliprv  33481  matunitlindf  36486  fdc  36613  grposnOLD  36750  rabren3dioph  41553  amgm2d  42950  amgm3d  42951  fourierdlem80  44902  sge0iun  45135  0ome  45245  issmflem  45443  2ffzoeq  46036  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  line2x  47440  line2y  47441  amgmw2d  47851