Description: Equality deduction for the sequence builder operation. (Contributed by Mario Carneiro, 7Sep2013)
Ref  Expression  

Hypothesis  seqeqd.1   ( ph > A = B ) 

Assertion  seqeq1d   ( ph > seq A ( .+ , F ) = seq B ( .+ , F ) ) 
Step  Hyp  Ref  Expression 

1  seqeqd.1   ( ph > A = B ) 

2  seqeq1   ( A = B > seq A ( .+ , F ) = seq B ( .+ , F ) ) 

3  1 2  syl   ( ph > seq A ( .+ , F ) = seq B ( .+ , F ) ) 