Theorem dfpred3g

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

	Ref	Expression
Assertion	dfpred3g	$$⊢X\in V\to Pred\left(R,A,X\right)=\left\{y\in A|yRX\right\}$$

Proof

Step	Hyp	Ref	Expression
1		predeq3	$$⊢x=X\to Pred\left(R,A,x\right)=Pred\left(R,A,X\right)$$
2		breq2	$$⊢x=X\to \left(yRx\leftrightarrow yRX\right)$$
3	2	rabbidv	$$⊢x=X\to \left\{y\in A|yRx\right\}=\left\{y\in A|yRX\right\}$$
4	1 3	eqeq12d	$$⊢x=X\to \left(Pred\left(R,A,x\right)=\left\{y\in A|yRx\right\}\leftrightarrow Pred\left(R,A,X\right)=\left\{y\in A|yRX\right\}\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	dfpred3	$$⊢Pred\left(R,A,x\right)=\left\{y\in A|yRx\right\}$$
7	4 6	vtoclg	$$⊢X\in V\to Pred\left(R,A,X\right)=\left\{y\in A|yRX\right\}$$