Theorem cosscnvssid3

Description: Equivalent expressions for the class of cosets by the converse of R to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021)

	Ref	Expression
Assertion	cosscnvssid3	|- ( ,~ `' R C_ _I <-> A. u A. v A. x ( ( u R x /\ v R x ) -> u = v ) )

Proof

Step	Hyp	Ref	Expression
1		cossssid3	|- ( ,~ `' R C_ _I <-> A. x A. u A. v ( ( x `' R u /\ x `' R v ) -> u = v ) )
2		alrot3	|- ( A. x A. u A. v ( ( x `' R u /\ x `' R v ) -> u = v ) <-> A. u A. v A. x ( ( x `' R u /\ x `' R v ) -> u = v ) )
3		brcnvg	|- ( ( x e. _V /\ u e. _V ) -> ( x `' R u <-> u R x ) )
4	3	el2v	|- ( x `' R u <-> u R x )
5		brcnvg	|- ( ( x e. _V /\ v e. _V ) -> ( x `' R v <-> v R x ) )
6	5	el2v	|- ( x `' R v <-> v R x )
7	4 6	anbi12i	|- ( ( x `' R u /\ x `' R v ) <-> ( u R x /\ v R x ) )
8	7	imbi1i	|- ( ( ( x `' R u /\ x `' R v ) -> u = v ) <-> ( ( u R x /\ v R x ) -> u = v ) )
9	8	3albii	|- ( A. u A. v A. x ( ( x `' R u /\ x `' R v ) -> u = v ) <-> A. u A. v A. x ( ( u R x /\ v R x ) -> u = v ) )
10	1 2 9	3bitri	|- ( ,~ `' R C_ _I <-> A. u A. v A. x ( ( u R x /\ v R x ) -> u = v ) )