Theorem feq2i 6728

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

Syntax hints:   ↔ wb 206   = wceq 1536  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-fn 6565  df-f 6566

This theorem is referenced by:  fresaun  6779  fmpox  8090  fmpo  8091  tposf  8277  issmo  8386  axdc3lem4  10490  cardf  10587  smobeth  10623  seqf2  14058  hashfxnn0  14372  snopiswrd  14557  iswrddm0  14572  s1dm  14642  s2dm  14925  s7f1o  15001  ntrivcvgtail  15932  vdwlem8  17021  0ram  17053  gsumws1  18863  ga0  19328  efgsp1  19769  efgsfo  19771  efgredleme  19775  efgred  19780  ablfaclem2  20120  islinds2  21850  rhmply1vsca  22407  pmatcollpw3fi1lem1  22807  0met  24391  dvef  26032  dvfsumrlim2  26087  dchrisum0  27578  noxp1o  27722  trgcgrg  28537  tgcgr4  28553  axlowdimlem4  28974  uhgr0e  29102  vtxdumgrval  29518  wlkp1  29713  pthdlem2  29800  0wlk  30144  0spth  30154  0clwlkv  30159  wlk2v2e  30185  wlkl0  30395  padct  32736  wrdpmtrlast  33095  mbfmcnt  34249  coinfliprv  34463  matunitlindf  37604  fdc  37731  grposnOLD  37868  rabren3dioph  42802  amgm2d  44187  amgm3d  44188  fourierdlem80  46141  sge0iun  46374  0ome  46484  issmflem  46682  2ffzoeq  47276  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  line2x  48603  line2y  48604  amgmw2d  49034