Theorem cossss

Description: Subclass theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 11-Nov-2019)

	Ref	Expression
Assertion	cossss	|- ( A C_ B -> ,~ A C_ ,~ B )

Proof

Step	Hyp	Ref	Expression
1		ssbr	|- ( A C_ B -> ( x A y -> x B y ) )
2		ssbr	|- ( A C_ B -> ( x A z -> x B z ) )
3	1 2	anim12d	|- ( A C_ B -> ( ( x A y /\ x A z ) -> ( x B y /\ x B z ) ) )
4	3	eximdv	|- ( A C_ B -> ( E. x ( x A y /\ x A z ) -> E. x ( x B y /\ x B z ) ) )
5	4	ssopab2dv	|- ( A C_ B -> { <. y , z >. | E. x ( x A y /\ x A z ) } C_ { <. y , z >. | E. x ( x B y /\ x B z ) } )
6		df-coss	|- ,~ A = { <. y , z >. | E. x ( x A y /\ x A z ) }
7		df-coss	|- ,~ B = { <. y , z >. | E. x ( x B y /\ x B z ) }
8	5 6 7	3sstr4g	|- ( A C_ B -> ,~ A C_ ,~ B )