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  10501  fseq1m1p1  10502  seqf  10901  seqf2  10905  seqf1og  10958  iswrdinn0  11309  wrdf  11310  iswrdiz  11311  wrdffz  11325  ffz0iswrdnn0  11331  wrdnval  11335  ccatalpha  11381  swrdf  11427  swrdwrdsymbg  11436  cats1un  11493  s2dmg  11562  intopsn  13687  resmhm  13794  gzsumwsubmcl  13801  gzsumwmhm  13803  isghm  14046  resghm  14063  gzsumsplit0  14148  gsumvalfi  14152  gzsumgsum  14155  psrelbasfi  15067  lmtopcnp  15351  ellimc3apf  15761  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dviaddf  15806  dvimulf  15807  dvcjbr  15809  dvcj  15810  dvrecap  15814  dvmptclx  15819  uhgrm  16319  wrdupgren  16337  upgrfnen  16339  wrdumgren  16347  umgrfnen  16349  upgr2wlkdc  16618  wlkres  16620