This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (R, A, X) \subseteq A$

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