Theorem feq2d 5501

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 5497	. 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 5353

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 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227  df-fn 5360  df-f 5361

This theorem is referenced by:  feq12d  5503  ffdm  5538  fsng  5855  fsn2g  5857  issmo2  6533  qliftf  6867  elpm2r  6913  casef  7392  fseq1p1m1  10450  fseq1m1p1  10451  seqf  10850  seqf2  10854  seqf1og  10907  iswrdinn0  11254  wrdf  11255  iswrdiz  11256  wrdffz  11270  ffz0iswrdnn0  11276  wrdnval  11280  ccatalpha  11326  swrdf  11372  swrdwrdsymbg  11381  cats1un  11438  s2dmg  11507  intopsn  13630  gsumprval  13662  resmhm  13742  gsumwsubmcl  13751  gsumwmhm  13753  isghm  13996  resghm  14013  gsumsplit0  14099  gfsumval  14102  gsumgfsum  14106  psrelbasfi  14957  lmtopcnp  15241  ellimc3apf  15651  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dviaddf  15696  dvimulf  15697  dvcjbr  15699  dvcj  15700  dvrecap  15704  dvmptclx  15709  uhgrm  16199  wrdupgren  16217  upgrfnen  16219  wrdumgren  16227  umgrfnen  16229  upgr2wlkdc  16498  wlkres  16500