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 ( ( A. x e. dom R x R x /\ Rel R ) , RefRel R , EqvRel R )

Proof

Step	Hyp	Ref	Expression
1		refrelredund2	|- redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , EqvRel R )
2		idrefALT	|- ( ( _I |` dom R ) C_ R <-> A. x e. dom R x R x )
3	2	anbi1i	|- ( ( ( _I |` dom R ) C_ R /\ Rel R ) <-> ( A. x e. dom R x R x /\ Rel R ) )
4	3	redundpbi1	|- ( redund ( ( ( _I |` dom R ) C_ R /\ Rel R ) , RefRel R , EqvRel R ) <-> redund ( ( A. x e. dom R x R x /\ Rel R ) , RefRel R , EqvRel R ) )
5	1 4	mpbi	|- redund ( ( A. x e. dom R x R x /\ Rel R ) , RefRel R , EqvRel R )