Theorem feq2d 5460

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 5456	. 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 5313

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 5320  df-f 5321

This theorem is referenced by:  feq12d  5462  ffdm  5493  fsng  5807  issmo2  6433  qliftf  6765  elpm2r  6811  casef  7251  fseq1p1m1  10286  fseq1m1p1  10287  seqf  10681  seqf2  10685  seqf1og  10738  iswrdinn0  11071  wrdf  11072  iswrdiz  11073  wrdffz  11087  ffz0iswrdnn0  11093  wrdnval  11097  swrdf  11182  swrdwrdsymbg  11191  cats1un  11248  s2dmg  11317  intopsn  13395  gsumprval  13427  resmhm  13515  gsumwsubmcl  13524  gsumwmhm  13526  isghm  13775  resghm  13792  psrelbasfi  14634  lmtopcnp  14918  ellimc3apf  15328  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dviaddf  15373  dvimulf  15374  dvcjbr  15376  dvcj  15377  dvrecap  15381  dvmptclx  15386  uhgrm  15872  wrdupgren  15890  upgrfnen  15892  wrdumgren  15900  umgrfnen  15902