Theorem predasetex

Description: The predecessor class exists when A does. (Contributed by Scott Fenton, 8-Feb-2011)

	Ref	Expression
Hypothesis	predasetex.1	$$⊢A\in \mathrm{V}$$
Assertion	predasetex	$$⊢Pred\left(R,A,X\right)\in \mathrm{V}$$

Proof

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