Theorem feq2d 5467

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 5463	. 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 5320

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 5327  df-f 5328

This theorem is referenced by:  feq12d  5469  ffdm  5502  fsng  5816  issmo2  6450  qliftf  6784  elpm2r  6830  casef  7278  fseq1p1m1  10319  fseq1m1p1  10320  seqf  10716  seqf2  10720  seqf1og  10773  iswrdinn0  11108  wrdf  11109  iswrdiz  11110  wrdffz  11124  ffz0iswrdnn0  11130  wrdnval  11134  ccatalpha  11180  swrdf  11226  swrdwrdsymbg  11235  cats1un  11292  s2dmg  11361  intopsn  13440  gsumprval  13472  resmhm  13560  gsumwsubmcl  13569  gsumwmhm  13571  isghm  13820  resghm  13837  psrelbasfi  14680  lmtopcnp  14964  ellimc3apf  15374  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dviaddf  15419  dvimulf  15420  dvcjbr  15422  dvcj  15423  dvrecap  15427  dvmptclx  15432  uhgrm  15919  wrdupgren  15937  upgrfnen  15939  wrdumgren  15947  umgrfnen  15949  upgr2wlkdc  16172  wlkres  16174