Metamath Proof Explorer

Theorem cossssid3

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 cossssid3 
|- ( ,~ R C_ _I <-> A. u A. x A. y ( ( u R x /\ u R y ) -> x = y ) )

Proof

Step Hyp Ref Expression
1 cossssid2 
 |-  ( ,~ R C_ _I <-> A. x A. y ( E. u ( u R x /\ u R y ) -> x = y ) )
2 19.23v 
 |-  ( A. u ( ( u R x /\ u R y ) -> x = y ) <-> ( E. u ( u R x /\ u R y ) -> x = y ) )
3 2 albii 
 |-  ( A. y A. u ( ( u R x /\ u R y ) -> x = y ) <-> A. y ( E. u ( u R x /\ u R y ) -> x = y ) )
4 alcom 
 |-  ( A. y A. u ( ( u R x /\ u R y ) -> x = y ) <-> A. u A. y ( ( u R x /\ u R y ) -> x = y ) )
5 3 4 bitr3i 
 |-  ( A. y ( E. u ( u R x /\ u R y ) -> x = y ) <-> A. u A. y ( ( u R x /\ u R y ) -> x = y ) )
6 5 albii 
 |-  ( A. x A. y ( E. u ( u R x /\ u R y ) -> x = y ) <-> A. x A. u A. y ( ( u R x /\ u R y ) -> x = y ) )
7 alcom 
 |-  ( A. x A. u A. y ( ( u R x /\ u R y ) -> x = y ) <-> A. u A. x A. y ( ( u R x /\ u R y ) -> x = y ) )
8 1 6 7 3bitri 
 |-  ( ,~ R C_ _I <-> A. u A. x A. y ( ( u R x /\ u R y ) -> x = y ) )