Metamath Proof Explorer


Theorem refrelredund2

Description: The naive version of the definition of reflexive relation is redundant with respect to reflexive relation (see dfrefrel2 ) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022)

Ref Expression
Assertion refrelredund2 redund I dom R R Rel R RefRel R EqvRel R

Proof

Step Hyp Ref Expression
1 refrelredund4 redund I dom R R Rel R RefRel R RefRel R SymRel R
2 df-eqvrel EqvRel R RefRel R SymRel R TrRel R
3 3simpa RefRel R SymRel R TrRel R RefRel R SymRel R
4 2 3 sylbi EqvRel R RefRel R SymRel R
5 4 redundpim3 redund I dom R R Rel R RefRel R RefRel R SymRel R redund I dom R R Rel R RefRel R EqvRel R
6 1 5 ax-mp redund I dom R R Rel R RefRel R EqvRel R