Theorem elpredg

Description: Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011) (Proof shortened by BJ, 16-Oct-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elpredgg	$$⊢\left(X\in B\wedge Y\in A\right)\to \left(Y\in Pred\left(R,A,X\right)\leftrightarrow \left(Y\in A\wedge YRX\right)\right)$$
2		ibar	$$⊢Y\in A\to \left(YRX\leftrightarrow \left(Y\in A\wedge YRX\right)\right)$$
3	2	bicomd	$$⊢Y\in A\to \left(\left(Y\in A\wedge YRX\right)\leftrightarrow YRX\right)$$
4	3	adantl	$$⊢\left(X\in B\wedge Y\in A\right)\to \left(\left(Y\in A\wedge YRX\right)\leftrightarrow YRX\right)$$
5	1 4	bitrd	$$⊢\left(X\in B\wedge Y\in A\right)\to \left(Y\in Pred\left(R,A,X\right)\leftrightarrow YRX\right)$$