Theorem feq2d 5412

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 5408	. 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 1372   -->wf 5266

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-fn 5273  df-f 5274

This theorem is referenced by:  feq12d  5414  ffdm  5445  fsng  5752  issmo2  6374  qliftf  6706  elpm2r  6752  casef  7189  fseq1p1m1  10215  fseq1m1p1  10216  seqf  10607  seqf2  10611  seqf1og  10664  iswrdinn0  10997  wrdf  10998  iswrdiz  10999  wrdffz  11013  wrdnval  11022  intopsn  13170  gsumprval  13202  resmhm  13290  gsumwsubmcl  13299  gsumwmhm  13301  isghm  13550  resghm  13567  psrelbasfi  14409  lmtopcnp  14693  ellimc3apf  15103  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dviaddf  15148  dvimulf  15149  dvcjbr  15151  dvcj  15152  dvrecap  15156  dvmptclx  15161