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
|- F/_ x R
nfwrecs.2
|- F/_ x A
nfwrecs.3
|- F/_ x F
Assertion nfwrecs
|- F/_ x wrecs ( R , A , F )

Proof

Step Hyp Ref Expression
1 nfwrecs.1
 |-  F/_ x R
2 nfwrecs.2
 |-  F/_ x A
3 nfwrecs.3
 |-  F/_ x F
4 df-wrecs
 |-  wrecs ( R , A , F ) = frecs ( R , A , ( F o. 2nd ) )
5 nfcv
 |-  F/_ x 2nd
6 3 5 nfco
 |-  F/_ x ( F o. 2nd )
7 1 2 6 nffrecs
 |-  F/_ x frecs ( R , A , ( F o. 2nd ) )
8 4 7 nfcxfr
 |-  F/_ x wrecs ( R , A , F )