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\in V\to Pred\left(R,A,X\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
2		inex1g	$$⊢A\in V\to A\cap R^{-1}\left[\left\{X\right\}\right]\in \mathrm{V}$$
3	1 2	eqeltrid	$$⊢A\in V\to Pred\left(R,A,X\right)\in \mathrm{V}$$