Definition df-ers 37836

Description: Define the class of equivalence relations on domain quotients (or: domain quotients restricted to equivalence relations).

The present definition of equivalence relation in set.mm df-er 8705 "is not standard", "somewhat cryptic", has no costant 0-ary class and does not follow the traditional transparent reflexive-symmetric-transitive relation way of definition of equivalence. Definitions df-eqvrels 37757, dfeqvrels2 37761, dfeqvrels3 37762 and df-eqvrel 37758, dfeqvrel2 37763, dfeqvrel3 37764 are fully transparent in this regard. However, they lack the domain component (dom 𝑅 = 𝐴) of the present df-er 8705. While we acknowledge the need of a domain component, the present df-er 8705 definition does not utilize the results revealed by the new theorems in the Partition-Equivalence Theorem part below (like pets 38025 and pet 38024). From those theorems follows that the natural domain of equivalence relations is

not 𝑅Domain𝐴 (i.e. dom 𝑅 = 𝐴 see brdomaing 35199),

but 𝑅 DomainQss 𝐴 (i.e. (dom 𝑅 / 𝑅) = 𝐴, see brdmqss 37819), see erimeq 37852 vs. prter3 38055.

While I'm sure we need both equivalence relation df-eqvrels 37757 and equivalence relation on domain quotient df-ers 37836, I'm not sure whether we need a third equivalence relation concept with the present dom 𝑅 = 𝐴 component as well: this needs further investigation. As a default I suppose that these two concepts df-eqvrels 37757 and df-ers 37836 are enough and named the predicate version of the one on domain quotient as the alternate version df-erALTV 37837 of the present df-er 8705. (Contributed by Peter Mazsa, 26-Jun-2021.)

Assertion

Ref	Expression
df-ers	⊢ Ers = ( DomainQss ↾ EqvRels )

Detailed syntax breakdown of Definition df-ers

Step	Hyp	Ref	Expression
1		cers 37371	. 2 class Ers
2		cdmqss 37369	. . 3 class DomainQss
3		ceqvrels 37362	. . 3 class EqvRels
4	2, 3	cres 5678	. 2 class ( DomainQss ↾ EqvRels )
5	1, 4	wceq 1541	1 wff Ers = ( DomainQss ↾ EqvRels )

This definition is referenced by:  brers  37840