Metamath Proof Explorer

Theorem elrefrels3

Description: Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019)

Ref Expression
Assertion elrefrels3 
|- ( R e. RefRels <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dfrefrels3 
 |-  RefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x = y -> x r y ) }
2 dmeq 
 |-  ( r = R -> dom r = dom R )
3 rneq 
 |-  ( r = R -> ran r = ran R )
4 breq 
 |-  ( r = R -> ( x r y <-> x R y ) )
5 4 imbi2d 
 |-  ( r = R -> ( ( x = y -> x r y ) <-> ( x = y -> x R y ) ) )
6 3 5 raleqbidv 
 |-  ( r = R -> ( A. y e. ran r ( x = y -> x r y ) <-> A. y e. ran R ( x = y -> x R y ) ) )
7 2 6 raleqbidv 
 |-  ( r = R -> ( A. x e. dom r A. y e. ran r ( x = y -> x r y ) <-> A. x e. dom R A. y e. ran R ( x = y -> x R y ) ) )
8 1 7 rabeqel 
 |-  ( R e. RefRels <-> ( A. x e. dom R A. y e. ran R ( x = y -> x R y ) /\ R e. Rels ) )