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

Metamath Proof Explorer

Theorem cosscnv

Description: Class of cosets by the converse of R (Contributed by Peter Mazsa, 17-Jun-2020)

Ref Expression
Assertion cosscnv 
|- ,~ `' R = { <. x , y >. | E. u ( x R u /\ y R u ) }

Proof

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