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