Metamath Proof Explorer

Theorem elcnvrefrels3

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021)

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

Proof

Step Hyp Ref Expression
1 dfcnvrefrels3 
 |-  CnvRefRels = { r e. Rels | A. x e. dom r A. y e. ran r ( x r y -> x = 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 imbi1d 
 |-  ( r = R -> ( ( x r y -> x = y ) <-> ( x R y -> x = y ) ) )
6 3 5 raleqbidv 
 |-  ( r = R -> ( A. y e. ran r ( x r y -> x = y ) <-> A. y e. ran R ( x R y -> x = y ) ) )
7 2 6 raleqbidv 
 |-  ( r = R -> ( A. x e. dom r A. y e. ran r ( x r y -> x = y ) <-> A. x e. dom R A. y e. ran R ( x R y -> x = y ) ) )
8 1 7 rabeqel 
 |-  ( R e. CnvRefRels <-> ( A. x e. dom R A. y e. ran R ( x R y -> x = y ) /\ R e. Rels ) )