Theorem feq2d 5413

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 5409	. 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 1373   -->wf 5267

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-fn 5274  df-f 5275

This theorem is referenced by:  feq12d  5415  ffdm  5446  fsng  5753  issmo2  6375  qliftf  6707  elpm2r  6753  casef  7190  fseq1p1m1  10216  fseq1m1p1  10217  seqf  10609  seqf2  10613  seqf1og  10666  iswrdinn0  10999  wrdf  11000  iswrdiz  11001  wrdffz  11015  wrdnval  11024  swrdf  11108  swrdwrdsymbg  11117  intopsn  13199  gsumprval  13231  resmhm  13319  gsumwsubmcl  13328  gsumwmhm  13330  isghm  13579  resghm  13596  psrelbasfi  14438  lmtopcnp  14722  ellimc3apf  15132  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dviaddf  15177  dvimulf  15178  dvcjbr  15180  dvcj  15181  dvrecap  15185  dvmptclx  15190