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