Theorem predbrg

Description: Closed form of elpredim . (Contributed by Scott Fenton, 13-Apr-2011) (Revised by NM, 5-Apr-2016)

	Ref	Expression
Assertion	predbrg	$$⊢\left(X\in V\wedge Y\in Pred\left(R,A,X\right)\right)\to YRX$$

Proof

Step	Hyp	Ref	Expression
1		predeq3	$$⊢x=X\to Pred\left(R,A,x\right)=Pred\left(R,A,X\right)$$
2	1	eleq2d	$$⊢x=X\to \left(Y\in Pred\left(R,A,x\right)\leftrightarrow Y\in Pred\left(R,A,X\right)\right)$$
3		breq2	$$⊢x=X\to \left(YRx\leftrightarrow YRX\right)$$
4	2 3	imbi12d	$$⊢x=X\to \left(\left(Y\in Pred\left(R,A,x\right)\to YRx\right)\leftrightarrow \left(Y\in Pred\left(R,A,X\right)\to YRX\right)\right)$$
5		vex	$$⊢x\in \mathrm{V}$$
6	5	elpredim	$$⊢Y\in Pred\left(R,A,x\right)\to YRx$$
7	4 6	vtoclg	$$⊢X\in V\to \left(Y\in Pred\left(R,A,X\right)\to YRX\right)$$
8	7	imp	$$⊢\left(X\in V\wedge Y\in Pred\left(R,A,X\right)\right)\to YRX$$