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

Metamath Proof Explorer

Theorem cosscnvssid3

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, 28-Jul-2021)

Ref Expression
Assertion cosscnvssid3 
|- ( ,~ `' R C_ _I <-> A. u A. v A. x ( ( u R x /\ v R x ) -> u = v ) )

Proof

Step Hyp Ref Expression
1 cossssid3 
 |-  ( ,~ `' R C_ _I <-> A. x A. u A. v ( ( x `' R u /\ x `' R v ) -> u = v ) )
2 alrot3 
 |-  ( A. x A. u A. v ( ( x `' R u /\ x `' R v ) -> u = v ) <-> A. u A. v A. x ( ( x `' R u /\ x `' R v ) -> u = v ) )
3 brcnvg 
 |-  ( ( x e. _V /\ u e. _V ) -> ( x `' R u <-> u R x ) )
4 3 el2v 
 |-  ( x `' R u <-> u R x )
5 brcnvg 
 |-  ( ( x e. _V /\ v e. _V ) -> ( x `' R v <-> v R x ) )
6 5 el2v 
 |-  ( x `' R v <-> v R x )
7 4 6 anbi12i 
 |-  ( ( x `' R u /\ x `' R v ) <-> ( u R x /\ v R x ) )
8 7 imbi1i 
 |-  ( ( ( x `' R u /\ x `' R v ) -> u = v ) <-> ( ( u R x /\ v R x ) -> u = v ) )
9 8 3albii 
 |-  ( A. u A. v A. x ( ( x `' R u /\ x `' R v ) -> u = v ) <-> A. u A. v A. x ( ( u R x /\ v R x ) -> u = v ) )
10 1 2 9 3bitri 
 |-  ( ,~ `' R C_ _I <-> A. u A. v A. x ( ( u R x /\ v R x ) -> u = v ) )