Metamath Proof Explorer


Theorem refrelsredund2

Description: The naive version of the class of reflexive relations is redundant with respect to the class of reflexive relations (see dfrefrels2 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

Ref Expression
Assertion refrelsredund2 r Rels | I dom r r Redund RefRels EqvRels

Proof

Step Hyp Ref Expression
1 refrelsredund4 r Rels | I dom r r Redund RefRels RefRels SymRels
2 df-eqvrels EqvRels = RefRels SymRels TrRels
3 inss1 RefRels SymRels TrRels RefRels SymRels
4 2 3 eqsstri EqvRels RefRels SymRels
5 4 redundss3 r Rels | I dom r r Redund RefRels RefRels SymRels r Rels | I dom r r Redund RefRels EqvRels
6 1 5 ax-mp r Rels | I dom r r Redund RefRels EqvRels