Theorem feq2d 5470

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
feq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
feq2d	|- ( ph -> ( F : A --> C <-> F : B --> C ) )

Proof of Theorem feq2d

Step	Hyp	Ref	Expression
1		feq2d.1	. 2 |- ( ph -> A = B )
2		feq2 5466	. 2 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )
3	1, 2	syl 14	1 |- ( ph -> ( F : A --> C <-> F : B --> C ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   -->wf 5322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5329  df-f 5330

This theorem is referenced by:  feq12d  5472  ffdm  5505  fsng  5820  issmo2  6454  qliftf  6788  elpm2r  6834  casef  7286  fseq1p1m1  10328  fseq1m1p1  10329  seqf  10725  seqf2  10729  seqf1og  10782  iswrdinn0  11117  wrdf  11118  iswrdiz  11119  wrdffz  11133  ffz0iswrdnn0  11139  wrdnval  11143  ccatalpha  11189  swrdf  11235  swrdwrdsymbg  11244  cats1un  11301  s2dmg  11370  intopsn  13449  gsumprval  13481  resmhm  13569  gsumwsubmcl  13578  gsumwmhm  13580  isghm  13829  resghm  13846  psrelbasfi  14689  lmtopcnp  14973  ellimc3apf  15383  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dviaddf  15428  dvimulf  15429  dvcjbr  15431  dvcj  15432  dvrecap  15436  dvmptclx  15441  uhgrm  15928  wrdupgren  15946  upgrfnen  15948  wrdumgren  15956  umgrfnen  15958  upgr2wlkdc  16227  wlkres  16229  gfsumval  16680  gsumgfsum  16684