Theorem feq2d 5396

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 5392	. 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 1364   -->wf 5255

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-fn 5262  df-f 5263

This theorem is referenced by:  feq12d  5398  ffdm  5429  fsng  5736  issmo2  6349  qliftf  6681  elpm2r  6727  casef  7156  fseq1p1m1  10172  fseq1m1p1  10173  seqf  10559  seqf2  10563  seqf1og  10616  iswrdinn0  10943  wrdf  10944  iswrdiz  10945  wrdffz  10959  wrdnval  10968  intopsn  13036  gsumprval  13068  resmhm  13145  gsumwsubmcl  13154  gsumwmhm  13156  isghm  13399  resghm  13416  lmtopcnp  14512  ellimc3apf  14922  dvidlemap  14953  dvidrelem  14954  dvidsslem  14955  dviaddf  14967  dvimulf  14968  dvcjbr  14970  dvcj  14971  dvrecap  14975  dvmptclx  14980