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} \subseteq R \land Rel R), RefRel R, EqvRel R)$

Proof

Step	Hyp	Ref	Expression
1		refrelredund4	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, (RefRel R \land SymRel R))$
2		df-eqvrel	$⊢ EqvRel R \leftrightarrow (RefRel R \land SymRel R \land TrRel R)$
3		3simpa	$⊢ (RefRel R \land SymRel R \land TrRel R) \to (RefRel R \land SymRel R)$
4	2 3	sylbi	$⊢ EqvRel R \to (RefRel R \land SymRel R)$
5	4	redundpim3	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, (RefRel R \land SymRel R)) \to redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, EqvRel R)$
6	1 5	ax-mp	$⊢ redund (({I ↾}_{dom R} \subseteq R \land Rel R), RefRel R, EqvRel R)$