Theorem cosscnvssid4

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, 31-Aug-2021)

	Ref	Expression
Assertion	cosscnvssid4	|- ( ,~ `' R C_ _I <-> A. x E* u u R x )

Proof

Step	Hyp	Ref	Expression
1		cossssid4	|- ( ,~ `' R C_ _I <-> A. x E* u x `' R u )
2		brcnvg	|- ( ( x e. _V /\ u e. _V ) -> ( x `' R u <-> u R x ) )
3	2	el2v	|- ( x `' R u <-> u R x )
4	3	mobii	|- ( E* u x `' R u <-> E* u u R x )
5	4	albii	|- ( A. x E* u x `' R u <-> A. x E* u u R x )
6	1 5	bitri	|- ( ,~ `' R C_ _I <-> A. x E* u u R x )