Theorem feq2d 5391

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 5387	. 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 1364   -->wf 5250

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-fn 5257  df-f 5258

This theorem is referenced by:  feq12d  5393  ffdm  5424  fsng  5731  issmo2  6342  qliftf  6674  elpm2r  6720  casef  7147  fseq1p1m1  10160  fseq1m1p1  10161  seqf  10535  seqf2  10539  seqf1og  10592  iswrdinn0  10919  wrdf  10920  iswrdiz  10921  wrdffz  10935  wrdnval  10944  intopsn  12950  gsumprval  12982  resmhm  13059  gsumwsubmcl  13068  gsumwmhm  13070  isghm  13313  resghm  13330  lmtopcnp  14418  ellimc3apf  14814  dvidlemap  14845  dviaddf  14854  dvimulf  14855  dvcjbr  14857  dvcj  14858  dvrecap  14862  dvmptclx  14865