Metamath Proof Explorer


Theorem recseq

Description: Equality theorem for recs . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Assertion recseq F=GrecsF=recsG

Proof

Step Hyp Ref Expression
1 wrecseq3 F=GwrecsEOnF=wrecsEOnG
2 df-recs recsF=wrecsEOnF
3 df-recs recsG=wrecsEOnG
4 1 2 3 3eqtr4g F=GrecsF=recsG