Theorem elpredgg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011) Generalize to closed form. (Revised by BJ, 16-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
2	1	elin2	$$⊢Y\in Pred\left(R,A,X\right)\leftrightarrow \left(Y\in A\wedge Y\in R^{-1}\left[\left\{X\right\}\right]\right)$$
3		elinisegg	$$⊢\left(X\in V\wedge Y\in W\right)\to \left(Y\in R^{-1}\left[\left\{X\right\}\right]\leftrightarrow YRX\right)$$
4	3	anbi2d	$$⊢\left(X\in V\wedge Y\in W\right)\to \left(\left(Y\in A\wedge Y\in R^{-1}\left[\left\{X\right\}\right]\right)\leftrightarrow \left(Y\in A\wedge YRX\right)\right)$$
5	2 4	bitrid	$$⊢\left(X\in V\wedge Y\in W\right)\to \left(Y\in Pred\left(R,A,X\right)\leftrightarrow \left(Y\in A\wedge YRX\right)\right)$$