Theorem feq2d 5524

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 5520	. 2 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )
3	1, 2	syl 14	1 |- ( ph -> ( F : A --> C <-> F : B --> C ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   -->wf 5376

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5383  df-f 5384

This theorem is used by:  feq12d  5526  ffdm  5561  fsng  5884  fsn2g  5886  issmo2  6564  qliftf  6898  elpm2r  6944  casef  7434  fseq1p1m1  10518  fseq1m1p1  10519  seqf  10922  seqf2  10926  seqf1og  10979  iswrdinn0  11331  wrdf  11332  iswrdiz  11333  wrdffz  11347  ffz0iswrdnn0  11353  wrdnval  11357  ccatalpha  11403  swrdf  11449  swrdwrdsymbg  11458  cats1un  11515  s2dmg  11584  intopsn  13746  resmhm  13853  gzsumwsubmcl  13860  gzsumwmhm  13862  isghm  14105  resghm  14122  gzsumsplit0  14238  gsumvalfi  14242  gzsumgsum  14245  gsummptfidmsplit  14254  psrelbasfi  15180  lmtopcnp  15476  ellimc3apf  15886  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dviaddf  15931  dvimulf  15932  dvcjbr  15934  dvcj  15935  dvrecap  15939  dvmptclx  15944  uhgrm  16524  wrdupgren  16542  upgrfnen  16544  wrdumgren  16552  umgrfnen  16554  upgr2wlkdc  16823  wlkres  16825