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 _xR
nfwsuc.2 _xA
nfwsuc.3 _xX
Assertion nfwsuc _xwsucRAX

Proof

Step Hyp Ref Expression
1 nfwsuc.1 _xR
2 nfwsuc.2 _xA
3 nfwsuc.3 _xX
4 df-wsuc wsucRAX=supPredR-1AXAR
5 1 nfcnv _xR-1
6 5 2 3 nfpred _xPredR-1AX
7 6 2 1 nfinf _xsupPredR-1AXAR
8 4 7 nfcxfr _xwsucRAX