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 CnvRefRels x dom R y ran R x R y x = y R Rels

Proof

Step Hyp Ref Expression
1 dfcnvrefrels3 CnvRefRels = r Rels | x dom r y 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 y ran r x r y x = y y ran R x R y x = y
7 2 6 raleqbidv r = R x dom r y ran r x r y x = y x dom R y ran R x R y x = y
8 1 7 rabeqel R CnvRefRels x dom R y ran R x R y x = y R Rels