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

Metamath Proof Explorer

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 )