Theorem feq2d 5268

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 5264	. 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 1332   -->wf 5127

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-fn 5134  df-f 5135

This theorem is referenced by:  feq12d  5270  ffdm  5301  fsng  5601  issmo2  6194  qliftf  6522  elpm2r  6568  casef  6981  fseq1p1m1  9905  fseq1m1p1  9906  seqf  10265  seqf2  10268  lmtopcnp  12458  ellimc3apf  12837  dvidlemap  12868  dviaddf  12877  dvimulf  12878  dvcjbr  12880  dvcj  12881  dvrecap  12885  dvmptclx  12888