Theorem feq2d 5516

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 5512	. 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 1402   -->wf 5368

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375  df-f 5376

This theorem is referenced by:  feq12d  5518  ffdm  5553  fsng  5872  fsn2g  5874  issmo2  6550  qliftf  6884  elpm2r  6930  casef  7418  fseq1p1m1  10479  fseq1m1p1  10480  seqf  10879  seqf2  10883  seqf1og  10936  iswrdinn0  11287  wrdf  11288  iswrdiz  11289  wrdffz  11303  ffz0iswrdnn0  11309  wrdnval  11313  ccatalpha  11359  swrdf  11405  swrdwrdsymbg  11414  cats1un  11471  s2dmg  11540  intopsn  13664  resmhm  13771  gzsumwsubmcl  13778  gzsumwmhm  13780  isghm  14023  resghm  14040  gzsumsplit0  14125  gsumvalfi  14129  gzsumgsum  14132  psrelbasfi  14990  lmtopcnp  15274  ellimc3apf  15684  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dviaddf  15729  dvimulf  15730  dvcjbr  15732  dvcj  15733  dvrecap  15737  dvmptclx  15742  uhgrm  16233  wrdupgren  16251  upgrfnen  16253  wrdumgren  16261  umgrfnen  16263  upgr2wlkdc  16532  wlkres  16534