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 )