Description: Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | dfrefrels3 | |- RefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x = y -> x r y ) } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfrefrels2 | |- RefRels = { r e. Rels | ( _I i^i ( dom r X. ran r ) ) C_ r } |
|
2 | idinxpss | |- ( ( _I i^i ( dom r X. ran r ) ) C_ r <-> A. x e. dom r A. y e. ran r ( x = y -> x r y ) ) |
|
3 | 1 2 | rabbieq | |- RefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x = y -> x r y ) } |