Theorem qsss1

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

	Ref	Expression
Assertion	qsss1	|- ( A C_ B -> ( A /. C ) C_ ( B /. C ) )

Proof

Step	Hyp	Ref	Expression
1		ssrexv	|- ( A C_ B -> ( E. x e. A y = [ x ] C -> E. x e. B y = [ x ] C ) )
2	1	ss2abdv	|- ( A C_ B -> { y | E. x e. A y = [ x ] C } C_ { y | E. x e. B y = [ x ] C } )
3		df-qs	|- ( A /. C ) = { y | E. x e. A y = [ x ] C }
4		df-qs	|- ( B /. C ) = { y | E. x e. B y = [ x ] C }
5	2 3 4	3sstr4g	|- ( A C_ B -> ( A /. C ) C_ ( B /. C ) )