Theorem predexg

Description: The predecessor class exists when A does. (Contributed by Scott Fenton, 8-Feb-2011) Generalize to closed form. (Revised by BJ, 27-Oct-2024)

	Ref	Expression
Assertion	predexg	|- ( A e. V -> Pred ( R , A , X ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-pred	|- Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
2		inex1g	|- ( A e. V -> ( A i^i ( `' R " { X } ) ) e. _V )
3	1 2	eqeltrid	|- ( A e. V -> Pred ( R , A , X ) e. _V )