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 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		refrelredund4	⊢ redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , ( RefRel 𝑅 ∧ SymRel 𝑅 ) )
2		df-eqvrel	⊢ ( EqvRel 𝑅 ↔ ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) )
3		3simpa	⊢ ( ( RefRel 𝑅 ∧ SymRel 𝑅 ∧ TrRel 𝑅 ) → ( RefRel 𝑅 ∧ SymRel 𝑅 ) )
4	2 3	sylbi	⊢ ( EqvRel 𝑅 → ( RefRel 𝑅 ∧ SymRel 𝑅 ) )
5	4	redundpim3	⊢ ( redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , ( RefRel 𝑅 ∧ SymRel 𝑅 ) ) → redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 ) )
6	1 5	ax-mp	⊢ redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 )