Theorem feq2d 5521

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 5517	. 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 5373

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 5380  df-f 5381

This theorem is used by:  feq12d  5523  ffdm  5558  fsng  5881  fsn2g  5883  issmo2  6560  qliftf  6894  elpm2r  6940  casef  7428  fseq1p1m1  10511  fseq1m1p1  10512  seqf  10914  seqf2  10918  seqf1og  10971  iswrdinn0  11323  wrdf  11324  iswrdiz  11325  wrdffz  11339  ffz0iswrdnn0  11345  wrdnval  11349  ccatalpha  11395  swrdf  11441  swrdwrdsymbg  11450  cats1un  11507  s2dmg  11576  intopsn  13736  resmhm  13843  gzsumwsubmcl  13850  gzsumwmhm  13852  isghm  14095  resghm  14112  gzsumsplit0  14197  gsumvalfi  14201  gzsumgsum  14204  psrelbasfi  15116  lmtopcnp  15400  ellimc3apf  15810  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dviaddf  15855  dvimulf  15856  dvcjbr  15858  dvcj  15859  dvrecap  15863  dvmptclx  15868  uhgrm  16417  wrdupgren  16435  upgrfnen  16437  wrdumgren  16445  umgrfnen  16447  upgr2wlkdc  16716  wlkres  16718