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 )