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

Metamath Proof Explorer

Theorem relss

Description: Subclass theorem for relation predicate. Theorem 2 of Suppes p. 58. (Contributed by NM, 15-Aug-1994)

		Ref	Expression
	Assertion	relss	$⊢ A \subseteq B \to (Rel B \to Rel A)$

Step	Hyp	Ref	Expression
1		sstr2	$⊢ A \subseteq B \to (B \subseteq V \times V \to A \subseteq V \times V)$
2		df-rel	$⊢ Rel B \leftrightarrow B \subseteq V \times V$
3		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
4	1 2 3	3imtr4g	$⊢ A \subseteq B \to (Rel B \to Rel A)$