Metamath Proof Explorer


Theorem refrelredund3

Description: The naive version of the definition of reflexive relation ( A. x e. dom R x R x /\ Rel R ) is redundant with respect to reflexive relation (see dfrefrel3 ) in equivalence relation. (Contributed by Peter Mazsa, 25-Oct-2022)

Ref Expression
Assertion refrelredund3 redund x dom R x R x Rel R RefRel R EqvRel R

Proof

Step Hyp Ref Expression
1 refrelredund2 redund I dom R R Rel R RefRel R EqvRel R
2 idrefALT I dom R R x dom R x R x
3 2 anbi1i I dom R R Rel R x dom R x R x Rel R
4 3 redundpbi1 redund I dom R R Rel R RefRel R EqvRel R redund x dom R x R x Rel R RefRel R EqvRel R
5 1 4 mpbi redund x dom R x R x Rel R RefRel R EqvRel R