Theorem cossssid2

Description: Equivalent expressions for the class of cosets by R to be a subset of the identity class. (Contributed by Peter Mazsa, 10-Mar-2019)

	Ref	Expression
Assertion	cossssid2	|- ( ,~ R C_ _I <-> A. x A. y ( E. u ( u R x /\ u R y ) -> x = y ) )

Proof

Step	Hyp	Ref	Expression
1		df-id	|- _I = { <. x , y >. | x = y }
2	1	sseq2i	|- ( ,~ R C_ _I <-> ,~ R C_ { <. x , y >. | x = y } )
3		df-coss	|- ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
4	3	sseq1i	|- ( ,~ R C_ { <. x , y >. | x = y } <-> { <. x , y >. | E. u ( u R x /\ u R y ) } C_ { <. x , y >. | x = y } )
5		ssopab2bw	|- ( { <. x , y >. | E. u ( u R x /\ u R y ) } C_ { <. x , y >. | x = y } <-> A. x A. y ( E. u ( u R x /\ u R y ) -> x = y ) )
6	2 4 5	3bitri	|- ( ,~ R C_ _I <-> A. x A. y ( E. u ( u R x /\ u R y ) -> x = y ) )