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

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 )