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  fsn2g  5822  issmo2  6455  qliftf  6789  elpm2r  6835  casef  7287  fseq1p1m1  10329  fseq1m1p1  10330  seqf  10727  seqf2  10731  seqf1og  10784  iswrdinn0  11122  wrdf  11123  iswrdiz  11124  wrdffz  11138  ffz0iswrdnn0  11144  wrdnval  11148  ccatalpha  11194  swrdf  11240  swrdwrdsymbg  11249  cats1un  11306  s2dmg  11375  intopsn  13455  gsumprval  13487  resmhm  13575  gsumwsubmcl  13584  gsumwmhm  13586  isghm  13835  resghm  13852  gsumsplit0  13938  psrelbasfi  14696  lmtopcnp  14980  ellimc3apf  15390  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dviaddf  15435  dvimulf  15436  dvcjbr  15438  dvcj  15439  dvrecap  15443  dvmptclx  15448  uhgrm  15935  wrdupgren  15953  upgrfnen  15955  wrdumgren  15963  umgrfnen  15965  upgr2wlkdc  16234  wlkres  16236  gfsumval  16707  gsumgfsum  16711