Metamath Proof Explorer

Theorem cosseq

Description: Equality theorem for the classes of cosets by A and B . (Contributed by Peter Mazsa, 9-Jan-2018)

Ref Expression
Assertion cosseq 
|- ( A = B -> ,~ A = ,~ B )

Proof

Step Hyp Ref Expression
1 breq 
 |-  ( A = B -> ( u A x <-> u B x ) )
2 breq 
 |-  ( A = B -> ( u A y <-> u B y ) )
3 1 2 anbi12d 
 |-  ( A = B -> ( ( u A x /\ u A y ) <-> ( u B x /\ u B y ) ) )
4 3 exbidv 
 |-  ( A = B -> ( E. u ( u A x /\ u A y ) <-> E. u ( u B x /\ u B y ) ) )
5 4 opabbidv 
 |-  ( A = B -> { <. x , y >. | E. u ( u A x /\ u A y ) } = { <. x , y >. | E. u ( u B x /\ u B y ) } )
6 df-coss 
 |-  ,~ A = { <. x , y >. | E. u ( u A x /\ u A y ) }
7 df-coss 
 |-  ,~ B = { <. x , y >. | E. u ( u B x /\ u B y ) }
8 5 6 7 3eqtr4g 
 |-  ( A = B -> ,~ A = ,~ B )