Metamath Proof Explorer


Theorem refrelsredund3

Description: The naive version of the class of reflexive relations { r e. Rels | A. x e. dom r x r x } is redundant with respect to the class of reflexive relations (see dfrefrels3 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Assertion refrelsredund3 r Rels | x dom r x r x Redund RefRels EqvRels

Proof

Step Hyp Ref Expression
1 refrelsredund2 r Rels | I dom r r Redund RefRels EqvRels
2 idrefALT I dom r r x dom r x r x
3 2 rabbii r Rels | I dom r r = r Rels | x dom r x r x
4 3 redundeq1 r Rels | I dom r r Redund RefRels EqvRels r Rels | x dom r x r x Redund RefRels EqvRels
5 1 4 mpbi r Rels | x dom r x r x Redund RefRels EqvRels