Theorem feq2d 5496

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 5492	. 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 1398   -->wf 5348

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-fn 5355  df-f 5356

This theorem is referenced by:  feq12d  5498  ffdm  5533  fsng  5850  fsn2g  5852  issmo2  6520  qliftf  6854  elpm2r  6900  casef  7379  fseq1p1m1  10428  fseq1m1p1  10429  seqf  10826  seqf2  10830  seqf1og  10883  iswrdinn0  11229  wrdf  11230  iswrdiz  11231  wrdffz  11245  ffz0iswrdnn0  11251  wrdnval  11255  ccatalpha  11301  swrdf  11347  swrdwrdsymbg  11356  cats1un  11413  s2dmg  11482  intopsn  13580  gsumprval  13612  resmhm  13700  gsumwsubmcl  13709  gsumwmhm  13711  isghm  13960  resghm  13977  gsumsplit0  14063  psrelbasfi  14831  lmtopcnp  15115  ellimc3apf  15525  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dviaddf  15570  dvimulf  15571  dvcjbr  15573  dvcj  15574  dvrecap  15578  dvmptclx  15583  uhgrm  16073  wrdupgren  16091  upgrfnen  16093  wrdumgren  16101  umgrfnen  16103  upgr2wlkdc  16372  wlkres  16374  gfsumval  16862  gsumgfsum  16866