Theorem wsucex

Description: Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

	Ref	Expression
Hypothesis	wsucex.1	|- ( ph -> R Or A )
Assertion	wsucex	|- ( ph -> wsuc ( R , A , X ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		wsucex.1	|- ( ph -> R Or A )
2		df-wsuc	|- wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )
3	1	infexd	|- ( ph -> inf ( Pred ( `' R , A , X ) , A , R ) e. _V )
4	2 3	eqeltrid	|- ( ph -> wsuc ( R , A , X ) e. _V )