Theorem predel

Description: Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011)

	Ref	Expression
Assertion	predel	$$⊢Y\in Pred\left(R,A,X\right)\to Y\in A$$

Proof

Step	Hyp	Ref	Expression
1		elinel1	$$⊢Y\in \left(A\cap R^{-1}\left[\left\{X\right\}\right]\right)\to Y\in A$$
2		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
3	1 2	eleq2s	$$⊢Y\in Pred\left(R,A,X\right)\to Y\in A$$