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

Metamath Proof Explorer

Theorem predpredss

Description: If A is a subset of B , then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011)

		Ref	Expression
	Assertion	predpredss	$⊢ A \subseteq B \to Pred (R, A, X) \subseteq Pred (R, B, X)$

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