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

Metamath Proof Explorer

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 ) }