Theorem feq2d 5433

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 5429	. 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 1373   -->wf 5286

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-fn 5293  df-f 5294

This theorem is referenced by:  feq12d  5435  ffdm  5466  fsng  5776  issmo2  6398  qliftf  6730  elpm2r  6776  casef  7216  fseq1p1m1  10251  fseq1m1p1  10252  seqf  10646  seqf2  10650  seqf1og  10703  iswrdinn0  11036  wrdf  11037  iswrdiz  11038  wrdffz  11052  wrdnval  11061  swrdf  11146  swrdwrdsymbg  11155  cats1un  11212  intopsn  13314  gsumprval  13346  resmhm  13434  gsumwsubmcl  13443  gsumwmhm  13445  isghm  13694  resghm  13711  psrelbasfi  14553  lmtopcnp  14837  ellimc3apf  15247  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dviaddf  15292  dvimulf  15293  dvcjbr  15295  dvcj  15296  dvrecap  15300  dvmptclx  15305  uhgrm  15789  wrdupgren  15807  upgrfnen  15809  wrdumgren  15817  umgrfnen  15819