Theorem feq2d 5255

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 5251	. 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 104   = wceq 1331   -->wf 5114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-fn 5121  df-f 5122

This theorem is referenced by:  feq12d  5257  ffdm  5288  fsng  5586  issmo2  6179  qliftf  6507  elpm2r  6553  casef  6966  fseq1p1m1  9867  fseq1m1p1  9868  seqf  10227  seqf2  10230  lmtopcnp  12408  ellimc3apf  12787  dvidlemap  12818  dviaddf  12827  dvimulf  12828  dvcjbr  12830  dvcj  12831  dvrecap  12835  dvmptclx  12838