This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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