Theorem feq2i 5950

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

Syntax hints:   ↔ wb 195   = wceq 1475  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807  df-f 5808

This theorem is referenced by:  fresaun  5988  fmpt2x  7125  fmpt2  7126  tposf  7267  issmo  7332  axdc3lem4  9158  cardf  9251  smobeth  9287  seqf2  12682  hashfxnn0  12986  hashfOLD  12988  snopiswrd  13169  iswrddm0  13184  s1dm  13241  s2dm  13485  ntrivcvgtail  14471  vdwlem8  15530  0ram  15562  gsumws1  17199  ga0  17554  efgsp1  17973  efgsfo  17975  efgredleme  17979  efgred  17984  ablfaclem2  18308  islinds2  19971  pmatcollpw3fi1lem1  20410  0met  21981  dvef  23547  dvfsumrlim2  23599  dchrisum0  25009  trgcgrg  25210  tgcgr4  25226  axlowdimlem4  25625  uhgr0e  25737  uhgra0  25838  umgra0  25854  0wlk  26075  0trl  26076  wlkntrl  26092  0spth  26101  constr1trl  26118  constr2wlk  26128  constr2trl  26129  usgra2wlkspthlem2  26148  constr3trllem3  26180  constr3trllem4  26181  padct  28885  mbfmcnt  29657  coinfliprv  29871  matunitlindf  32577  fdc  32711  grposnOLD  32851  rabren3dioph  36397  amgm2d  37523  amgm3d  37524  fco3  38416  fourierdlem80  39079  sge0iun  39312  0ome  39419  issmflem  39613  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  2ffzoeq  40361  vtxdumgrval  40701  1wlkp1  40890  pthdlem2  40974  01wlk  41284  0spth-av  41294  1wlk2v2e  41324  amgmw2d  42359