Theorem feq2d 5353

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 5349	. 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 1353   -->wf 5212

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5219  df-f 5220

This theorem is referenced by:  feq12d  5355  ffdm  5386  fsng  5689  issmo2  6289  qliftf  6619  elpm2r  6665  casef  7086  fseq1p1m1  10093  fseq1m1p1  10094  seqf  10460  seqf2  10463  intopsn  12785  lmtopcnp  13720  ellimc3apf  14099  dvidlemap  14130  dviaddf  14139  dvimulf  14140  dvcjbr  14142  dvcj  14143  dvrecap  14147  dvmptclx  14150