Theorem bnj1418

Description: Property of _pred . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj1418	$$⊢y\in pred\left(x,A,R\right)\to yRx$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢z=y\to \left(zRx\leftrightarrow yRx\right)$$
2		df-bnj14	$$⊢pred\left(x,A,R\right)=\left\{z\in A|zRx\right\}$$
3	2	bnj1538	$$⊢z\in pred\left(x,A,R\right)\to zRx$$
4	1 3	vtoclga	$$⊢y\in pred\left(x,A,R\right)\to yRx$$