Theorem feq2d 5325

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 5321	. 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 1343   -->wf 5184

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-fn 5191  df-f 5192

This theorem is referenced by:  feq12d  5327  ffdm  5358  fsng  5658  issmo2  6257  qliftf  6586  elpm2r  6632  casef  7053  fseq1p1m1  10029  fseq1m1p1  10030  seqf  10396  seqf2  10399  intopsn  12598  lmtopcnp  12890  ellimc3apf  13269  dvidlemap  13300  dviaddf  13309  dvimulf  13310  dvcjbr  13312  dvcj  13313  dvrecap  13317  dvmptclx  13320