Metamath Proof Explorer


Theorem nfwrecs

Description: Bound-variable hypothesis builder for the well-ordered recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018) (Proof shortened by Scott Fenton, 17-Nov-2024)

Ref Expression
Hypotheses nfwrecs.1 _xR
nfwrecs.2 _xA
nfwrecs.3 _xF
Assertion nfwrecs _xwrecsRAF

Proof

Step Hyp Ref Expression
1 nfwrecs.1 _xR
2 nfwrecs.2 _xA
3 nfwrecs.3 _xF
4 df-wrecs wrecsRAF=frecsRAF2nd
5 nfcv _x2nd
6 3 5 nfco _xF2nd
7 1 2 6 nffrecs _xfrecsRAF2nd
8 4 7 nfcxfr _xwrecsRAF