Theorem bnj1152

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj1152	$$⊢Y\in pred\left(X,A,R\right)\leftrightarrow \left(Y\in A\wedge YRX\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢y=Y\to \left(yRX\leftrightarrow YRX\right)$$
2		df-bnj14	$$⊢pred\left(X,A,R\right)=\left\{y\in A|yRX\right\}$$
3	1 2	elrab2	$$⊢Y\in pred\left(X,A,R\right)\leftrightarrow \left(Y\in A\wedge YRX\right)$$