Metamath Proof Explorer


Theorem dfcoss3

Description: Alternate definition of the class of cosets by R (see the comment of df-coss ). (Contributed by Peter Mazsa, 27-Dec-2018)

Ref Expression
Assertion dfcoss3
|- ,~ R = ( R o. `' R )

Proof

Step Hyp Ref Expression
1 brcnvg
 |-  ( ( x e. _V /\ u e. _V ) -> ( x `' R u <-> u R x ) )
2 1 el2v
 |-  ( x `' R u <-> u R x )
3 2 anbi1i
 |-  ( ( x `' R u /\ u R y ) <-> ( u R x /\ u R y ) )
4 3 exbii
 |-  ( E. u ( x `' R u /\ u R y ) <-> E. u ( u R x /\ u R y ) )
5 4 opabbii
 |-  { <. x , y >. | E. u ( x `' R u /\ u R y ) } = { <. x , y >. | E. u ( u R x /\ u R y ) }
6 df-co
 |-  ( R o. `' R ) = { <. x , y >. | E. u ( x `' R u /\ u R y ) }
7 df-coss
 |-  ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
8 5 6 7 3eqtr4ri
 |-  ,~ R = ( R o. `' R )