Definition df-membparts

Description: Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021)

	Ref	Expression
Assertion	df-membparts	$$⊢\mathrm{MembParts}=\left\{a|\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmembparts	$$class\mathrm{MembParts}$$
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		cparts	$$class\mathrm{Parts}$$
7	5 4 6	wbr	$$wff\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a$$
8	7 1	cab	$$class\left\{a|\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\right\}$$
9	0 8	wceq	$$wff\mathrm{MembParts}=\left\{a|\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\mathrm{Parts}a\right\}$$