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  7429  fseq1p1m1  10512  fseq1m1p1  10513  seqf  10916  seqf2  10920  seqf1og  10973  iswrdinn0  11325  wrdf  11326  iswrdiz  11327  wrdffz  11341  ffz0iswrdnn0  11347  wrdnval  11351  ccatalpha  11397  swrdf  11443  swrdwrdsymbg  11452  cats1un  11509  s2dmg  11578  intopsn  13740  resmhm  13847  gzsumwsubmcl  13854  gzsumwmhm  13856  isghm  14099  resghm  14116  gzsumsplit0  14232  gsumvalfi  14236  gzsumgsum  14239  psrelbasfi  15152  lmtopcnp  15442  ellimc3apf  15852  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dviaddf  15897  dvimulf  15898  dvcjbr  15900  dvcj  15901  dvrecap  15905  dvmptclx  15910  uhgrm  16485  wrdupgren  16503  upgrfnen  16505  wrdumgren  16513  umgrfnen  16515  upgr2wlkdc  16784  wlkres  16786