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 ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		refrelredund2	⊢ redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 )
2		idrefALT	⊢ ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ↔ ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 )
3	2	anbi1i	⊢ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) ↔ ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ Rel 𝑅 ) )
4	3	redundpbi1	⊢ ( redund ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 ) ↔ redund ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 ) )
5	1 4	mpbi	⊢ redund ( ( ∀ 𝑥 ∈ dom 𝑅 𝑥 𝑅 𝑥 ∧ Rel 𝑅 ) , RefRel 𝑅 , EqvRel 𝑅 )