Definition df-members

Description: Define the class of membership equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022) (Revised by Peter Mazsa, 24-Jul-2023)

	Ref	Expression
Assertion	df-members	$$⊢\mathrm{MembErs}=\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmembers	$$class\mathrm{MembErs}$$
1		va	$$setvara$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	1	cv	$$setvara$$
5	3 4	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
6	5	ccoss	$$class\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
7		cers	$$class\mathrm{Ers}$$
8	6 4 7	wbr	$$wff\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a$$
9	8 1	cab	$$class\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right\}$$
10	0 9	wceq	$$wff\mathrm{MembErs}=\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Ers}a\right\}$$