Theorem feq2d 5395

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 5391	. 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 5254

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 5261  df-f 5262

This theorem is referenced by:  feq12d  5397  ffdm  5428  fsng  5735  issmo2  6347  qliftf  6679  elpm2r  6725  casef  7154  fseq1p1m1  10169  fseq1m1p1  10170  seqf  10556  seqf2  10560  seqf1og  10613  iswrdinn0  10940  wrdf  10941  iswrdiz  10942  wrdffz  10956  wrdnval  10965  intopsn  13010  gsumprval  13042  resmhm  13119  gsumwsubmcl  13128  gsumwmhm  13130  isghm  13373  resghm  13390  lmtopcnp  14486  ellimc3apf  14896  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dviaddf  14941  dvimulf  14942  dvcjbr  14944  dvcj  14945  dvrecap  14949  dvmptclx  14954