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 ((\forall x \in dom R x R x \land Rel R), RefRel R, EqvRel R)$

Proof

Step	Hyp	Ref	Expression
1		refrelredund2	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, EqvRel R)$
2		idrefALT	$⊢ {I ↾}_{dom R} \subseteq R \leftrightarrow \forall x \in dom R x R x$
3	2	anbi1i	$⊢ ({I ↾}_{dom R} \subseteq R \land Rel R) \leftrightarrow (\forall x \in dom R x R x \land Rel R)$
4	3	redundpbi1	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, EqvRel R) \leftrightarrow redund ((\forall x \in dom R x R x \land Rel R), RefRel R, EqvRel R)$
5	1 4	mpbi	$⊢ redund ((\forall x \in dom R x R x \land Rel R), RefRel R, EqvRel R)$

Metamath Proof Explorer

Theorem refrelredund3

Proof