Metamath Proof Explorer


Theorem nfwsuc

Description: Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

Ref Expression
Hypotheses nfwsuc.1
|- F/_ x R
nfwsuc.2
|- F/_ x A
nfwsuc.3
|- F/_ x X
Assertion nfwsuc
|- F/_ x wsuc ( R , A , X )

Proof

Step Hyp Ref Expression
1 nfwsuc.1
 |-  F/_ x R
2 nfwsuc.2
 |-  F/_ x A
3 nfwsuc.3
 |-  F/_ x X
4 df-wsuc
 |-  wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )
5 1 nfcnv
 |-  F/_ x `' R
6 5 2 3 nfpred
 |-  F/_ x Pred ( `' R , A , X )
7 6 2 1 nfinf
 |-  F/_ x inf ( Pred ( `' R , A , X ) , A , R )
8 4 7 nfcxfr
 |-  F/_ x wsuc ( R , A , X )