Metamath Proof Explorer


Theorem wrecseq1

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

Ref Expression
Assertion wrecseq1 R=SwrecsRAF=wrecsSAF

Proof

Step Hyp Ref Expression
1 eqid A=A
2 eqid F=F
3 wrecseq123 R=SA=AF=FwrecsRAF=wrecsSAF
4 1 2 3 mp3an23 R=SwrecsRAF=wrecsSAF