Theorem refrelsredund3

Description: The naive version of the class of reflexive relations { r e. Rels | A. x e. dom r x r x } is redundant with respect to the class of reflexive relations (see dfrefrels3 ) in the class of equivalence relations. (Contributed by Peter Mazsa, 26-Oct-2022)

	Ref	Expression
Assertion	refrelsredund3	|- { r e. Rels | A. x e. dom r x r x } Redund <. RefRels , EqvRels >.

Proof

Step	Hyp	Ref	Expression
1		refrelsredund2	|- { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , EqvRels >.
2		idrefALT	|- ( ( _I |` dom r ) C_ r <-> A. x e. dom r x r x )
3	2	rabbii	|- { r e. Rels | ( _I |` dom r ) C_ r } = { r e. Rels | A. x e. dom r x r x }
4	3	redundeq1	|- ( { r e. Rels | ( _I |` dom r ) C_ r } Redund <. RefRels , EqvRels >. <-> { r e. Rels | A. x e. dom r x r x } Redund <. RefRels , EqvRels >. )
5	1 4	mpbi	|- { r e. Rels | A. x e. dom r x r x } Redund <. RefRels , EqvRels >.