Metamath Proof Explorer


Theorem dfrefrels3

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

Proof

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