Theorem feq2i 6662

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

Syntax hints:   ↔ wb 206   = wceq 1542  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6503  df-f 6504

This theorem is referenced by:  fresaun  6713  fmpox  8021  fmpo  8022  tposf  8206  issmo  8290  axdc3lem4  10375  cardf  10472  smobeth  10509  seqf2  13956  hashfxnn0  14272  snopiswrd  14458  iswrddm0  14473  s1dm  14544  s2dm  14825  s7f1o  14901  ntrivcvgtail  15835  vdwlem8  16928  0ram  16960  gsumws1  18775  ga0  19239  efgsp1  19678  efgsfo  19680  efgredleme  19684  efgred  19689  ablfaclem2  20029  islinds2  21780  rhmply1vsca  22344  pmatcollpw3fi1lem1  22742  0met  24322  dvef  25952  dvfsumrlim2  26007  dchrisum0  27499  noxp1o  27643  trgcgrg  28599  tgcgr4  28615  axlowdimlem4  29030  uhgr0e  29156  vtxdumgrval  29572  wlkp1  29765  pthdlem2  29853  0wlk  30203  0spth  30213  0clwlkv  30218  wlk2v2e  30244  wlkl0  30454  padct  32807  wrdpmtrlast  33186  mbfmcnt  34445  coinfliprv  34660  matunitlindf  37866  fdc  37993  grposnOLD  38130  rabren3dioph  43169  amgm2d  44551  amgm3d  44552  fourierdlem80  46541  sge0iun  46774  0ome  46884  issmflem  47082  2ffzoeq  47684  nnsum4primesodd  48153  nnsum4primesoddALTV  48154  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  line2x  49111  line2y  49112  amgmw2d  50160