Theorem dfpred2

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 8-Feb-2011)

	Ref	Expression
Hypothesis	dfpred2.1	$$⊢X\in \mathrm{V}$$
Assertion	dfpred2	$$⊢Pred\left(R,A,X\right)=A\cap \left\{y|yRX\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfpred2.1	$$⊢X\in \mathrm{V}$$
2		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
3		iniseg	$$⊢X\in \mathrm{V}\to R^{-1}\left[\left\{X\right\}\right]=\left\{y|yRX\right\}$$
4	1 3	ax-mp	$$⊢R^{-1}\left[\left\{X\right\}\right]=\left\{y|yRX\right\}$$
5	4	ineq2i	$$⊢A\cap R^{-1}\left[\left\{X\right\}\right]=A\cap \left\{y|yRX\right\}$$
6	2 5	eqtri	$$⊢Pred\left(R,A,X\right)=A\cap \left\{y|yRX\right\}$$