Metamath Proof Explorer


Theorem wrecseq2

Description: Equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018)

Ref Expression
Assertion wrecseq2 A=BwrecsRAF=wrecsRBF

Proof

Step Hyp Ref Expression
1 eqid R=R
2 eqid F=F
3 wrecseq123 R=RA=BF=FwrecsRAF=wrecsRBF
4 1 2 3 mp3an13 A=BwrecsRAF=wrecsRBF