Theorem qsss1

Description: Subclass theorem for quotient sets. (Contributed by Peter Mazsa, 12-Sep-2020)

	Ref	Expression
Assertion	qsss1	$$⊢A\subseteq B\to A/C\subseteq B/C$$

Proof

Step	Hyp	Ref	Expression
1		ssrexv	$$⊢A\subseteq B\to \left(\exists x\in Ay=\left[x\right]C\to \exists x\in By=\left[x\right]C\right)$$
2	1	ss2abdv	$$⊢A\subseteq B\to \left\{y|\exists x\in Ay=\left[x\right]C\right\}\subseteq \left\{y|\exists x\in By=\left[x\right]C\right\}$$
3		df-qs	$$⊢A/C=\left\{y|\exists x\in Ay=\left[x\right]C\right\}$$
4		df-qs	$$⊢B/C=\left\{y|\exists x\in By=\left[x\right]C\right\}$$
5	2 3 4	3sstr4g	$$⊢A\subseteq B\to A/C\subseteq B/C$$