Theorem dfcoss2

Description: Alternate definition of the class of cosets by R : x and y are cosets by R iff there exists a set u such that both x and y are are elements of the R -coset of u (see also the comment of dfec2 ). R is usually a relation. (Contributed by Peter Mazsa, 16-Jan-2018)

	Ref	Expression
Assertion	dfcoss2	|- ,~ R = { <. x , y >. | E. u ( x e. [ u ] R /\ y e. [ u ] R ) }

Proof

Step	Hyp	Ref	Expression
1		df-coss	|- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
2		elecALTV	|- ( ( u e. _V /\ x e. _V ) -> ( x e. [ u ] R <-> u R x ) )
3	2	el2v	|- ( x e. [ u ] R <-> u R x )
4		elecALTV	|- ( ( u e. _V /\ y e. _V ) -> ( y e. [ u ] R <-> u R y ) )
5	4	el2v	|- ( y e. [ u ] R <-> u R y )
6	3 5	anbi12i	|- ( ( x e. [ u ] R /\ y e. [ u ] R ) <-> ( u R x /\ u R y ) )
7	6	exbii	|- ( E. u ( x e. [ u ] R /\ y e. [ u ] R ) <-> E. u ( u R x /\ u R y ) )
8	7	opabbii	|- { <. x , y >. | E. u ( x e. [ u ] R /\ y e. [ u ] R ) } = { <. x , y >. | E. u ( u R x /\ u R y ) }
9	1 8	eqtr4i	|- ,~ R = { <. x , y >. | E. u ( x e. [ u ] R /\ y e. [ u ] R ) }