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

Metamath Proof Explorer

Theorem dfeqvrels3

Description: Alternate definition of the class of equivalence relations. (Contributed by Peter Mazsa, 2-Dec-2019)

Ref Expression
Assertion dfeqvrels3 
|- EqvRels = { r e. Rels | ( A. x e. dom r x r x /\ A. x A. y ( x r y -> y r x ) /\ A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) ) }

Proof

Step Hyp Ref Expression
1 dfeqvrels2 
 |-  EqvRels = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) }
2 idrefALT 
 |-  ( ( _I |` dom r ) C_ r <-> A. x e. dom r x r x )
3 cnvsym 
 |-  ( `' r C_ r <-> A. x A. y ( x r y -> y r x ) )
4 cotr 
 |-  ( ( r o. r ) C_ r <-> A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) )
5 2 3 4 3anbi123i 
 |-  ( ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) <-> ( A. x e. dom r x r x /\ A. x A. y ( x r y -> y r x ) /\ A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) ) )
6 1 5 rabbieq 
 |-  EqvRels = { r e. Rels | ( A. x e. dom r x r x /\ A. x A. y ( x r y -> y r x ) /\ A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) ) }