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 u u A x u A y u u B x u B y
5 4 opabbidv A = B x y | u u A x u A y = x y | u u B x u B y
6 df-coss A = x y | u u A x u A y
7 df-coss B = x y | u u B x u B y
8 5 6 7 3eqtr4g A = B A = B