Theorem feq2d 5496

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 5492	. 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 1398   -->wf 5348

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-fn 5355  df-f 5356

This theorem is referenced by:  feq12d  5498  ffdm  5533  fsng  5850  fsn2g  5852  issmo2  6520  qliftf  6854  elpm2r  6900  casef  7379  fseq1p1m1  10428  fseq1m1p1  10429  seqf  10826  seqf2  10830  seqf1og  10883  iswrdinn0  11227  wrdf  11228  iswrdiz  11229  wrdffz  11243  ffz0iswrdnn0  11249  wrdnval  11253  ccatalpha  11299  swrdf  11345  swrdwrdsymbg  11354  cats1un  11411  s2dmg  11480  intopsn  13578  gsumprval  13610  resmhm  13698  gsumwsubmcl  13707  gsumwmhm  13709  isghm  13958  resghm  13975  gsumsplit0  14061  psrelbasfi  14829  lmtopcnp  15113  ellimc3apf  15523  dvidlemap  15554  dvidrelem  15555  dvidsslem  15556  dviaddf  15568  dvimulf  15569  dvcjbr  15571  dvcj  15572  dvrecap  15576  dvmptclx  15581  uhgrm  16071  wrdupgren  16089  upgrfnen  16091  wrdumgren  16099  umgrfnen  16101  upgr2wlkdc  16370  wlkres  16372  gfsumval  16860  gsumgfsum  16864