Theorem feq2d 5477

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 5473	. 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 5329

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 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5336  df-f 5337

This theorem is referenced by:  feq12d  5479  ffdm  5513  fsng  5828  fsn2g  5830  issmo2  6498  qliftf  6832  elpm2r  6878  casef  7330  fseq1p1m1  10374  fseq1m1p1  10375  seqf  10772  seqf2  10776  seqf1og  10829  iswrdinn0  11167  wrdf  11168  iswrdiz  11169  wrdffz  11183  ffz0iswrdnn0  11189  wrdnval  11193  ccatalpha  11239  swrdf  11285  swrdwrdsymbg  11294  cats1un  11351  s2dmg  11420  intopsn  13513  gsumprval  13545  resmhm  13633  gsumwsubmcl  13642  gsumwmhm  13644  isghm  13893  resghm  13910  gsumsplit0  13996  psrelbasfi  14760  lmtopcnp  15044  ellimc3apf  15454  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dviaddf  15499  dvimulf  15500  dvcjbr  15502  dvcj  15503  dvrecap  15507  dvmptclx  15512  uhgrm  16002  wrdupgren  16020  upgrfnen  16022  wrdumgren  16030  umgrfnen  16032  upgr2wlkdc  16301  wlkres  16303  gfsumval  16792  gsumgfsum  16796