Theorem feq2d 5461

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 5457	. 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 1395   -->wf 5314

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-fn 5321  df-f 5322

This theorem is referenced by:  feq12d  5463  ffdm  5496  fsng  5810  issmo2  6441  qliftf  6775  elpm2r  6821  casef  7266  fseq1p1m1  10302  fseq1m1p1  10303  seqf  10698  seqf2  10702  seqf1og  10755  iswrdinn0  11089  wrdf  11090  iswrdiz  11091  wrdffz  11105  ffz0iswrdnn0  11111  wrdnval  11115  ccatalpha  11161  swrdf  11202  swrdwrdsymbg  11211  cats1un  11268  s2dmg  11337  intopsn  13415  gsumprval  13447  resmhm  13535  gsumwsubmcl  13544  gsumwmhm  13546  isghm  13795  resghm  13812  psrelbasfi  14655  lmtopcnp  14939  ellimc3apf  15349  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dviaddf  15394  dvimulf  15395  dvcjbr  15397  dvcj  15398  dvrecap  15402  dvmptclx  15407  uhgrm  15893  wrdupgren  15911  upgrfnen  15913  wrdumgren  15921  umgrfnen  15923  upgr2wlkdc  16116  wlkres  16118