Theorem cnvcosseq

Description: The converse of cosets by R are cosets by R . (Contributed by Peter Mazsa, 3-May-2019)

	Ref	Expression
Assertion	cnvcosseq	|- `' ,~ R = ,~ R

Proof

Step	Hyp	Ref	Expression
1		brcosscnvcoss	|- ( ( x e. _V /\ y e. _V ) -> ( x ,~ R y <-> y ,~ R x ) )
2	1	el2v	|- ( x ,~ R y <-> y ,~ R x )
3	2	biimpi	|- ( x ,~ R y -> y ,~ R x )
4	3	gen2	|- A. x A. y ( x ,~ R y -> y ,~ R x )
5		cnvsym	|- ( `' ,~ R C_ ,~ R <-> A. x A. y ( x ,~ R y -> y ,~ R x ) )
6	4 5	mpbir	|- `' ,~ R C_ ,~ R
7		relcoss	|- Rel ,~ R
8		relcnveq	|- ( Rel ,~ R -> ( `' ,~ R C_ ,~ R <-> `' ,~ R = ,~ R ) )
9	7 8	ax-mp	|- ( `' ,~ R C_ ,~ R <-> `' ,~ R = ,~ R )
10	6 9	mpbi	|- `' ,~ R = ,~ R