Definition df-membpart

Description: Define the member partition predicate, or the disjoint restricted element relation on its domain quotient predicate. (Read: A is a member partition.) A alternative definition is dfmembpart2 .

Member partition is the conventional meaning of partition (see the notes of df-parts and dfmembpart2 ), we generalize the concept in df-parts and df-part .

Member partition and comember equivalence are the same by mpet . (Contributed by Peter Mazsa, 26-Jun-2021)

	Ref	Expression
Assertion	df-membpart	$$⊢MembPartA\leftrightarrow \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)PartA$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wmembpart	$$wffMembPartA$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	3 0	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
5	0 4	wpart	$$wff\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)PartA$$
6	1 5	wb	$$wff\left(MembPartA\leftrightarrow \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)PartA\right)$$