Metamath Proof Explorer

Theorem cossssid4

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

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

Proof

Step Hyp Ref Expression
1 cossssid3 
 |-  ( ,~ R C_ _I <-> A. u A. x A. y ( ( u R x /\ u R y ) -> x = y ) )
2 breq2 
 |-  ( x = y -> ( u R x <-> u R y ) )
3 2 mo4 
 |-  ( E* x u R x <-> A. x A. y ( ( u R x /\ u R y ) -> x = y ) )
4 3 albii 
 |-  ( A. u E* x u R x <-> A. u A. x A. y ( ( u R x /\ u R y ) -> x = y ) )
5 1 4 bitr4i 
 |-  ( ,~ R C_ _I <-> A. u E* x u R x )