Theorem dfpred3

Description: An alternate definition of predecessor class when X is a set. (Contributed by Scott Fenton, 13-Jun-2018)

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

Proof

Step	Hyp	Ref	Expression
1		dfpred2.1	$$⊢X\in \mathrm{V}$$
2		incom	$$⊢A\cap \left\{y|yRX\right\}=\left\{y|yRX\right\}\cap A$$
3	1	dfpred2	$$⊢Pred\left(R,A,X\right)=A\cap \left\{y|yRX\right\}$$
4		dfrab2	$$⊢\left\{y\in A|yRX\right\}=\left\{y|yRX\right\}\cap A$$
5	2 3 4	3eqtr4i	$$⊢Pred\left(R,A,X\right)=\left\{y\in A|yRX\right\}$$