Theorem predss

Description: The predecessor class of A is a subset of A . (Contributed by Scott Fenton, 2-Feb-2011)

	Ref	Expression
Assertion	predss	$$⊢Pred\left(R,A,X\right)\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		df-pred	$$⊢Pred\left(R,A,X\right)=A\cap R^{-1}\left[\left\{X\right\}\right]$$
2		inss1	$$⊢A\cap R^{-1}\left[\left\{X\right\}\right]\subseteq A$$
3	1 2	eqsstri	$$⊢Pred\left(R,A,X\right)\subseteq A$$