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 \left(\mathrm{Rel}B\to \mathrm{Rel}A\right)$$

Proof

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