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	Could not format assertion : No typesetting found for |- ( MembPart A <-> ( `' _E |` A ) Part A ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wmembpart	Could not format MembPart A : No typesetting found for wff MembPart A with typecode wff
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	Could not format ( `' _E |` A ) Part A : No typesetting found for wff ( `' _E |` A ) Part A with typecode wff
6	1 5	wb	Could not format ( MembPart A <-> ( `' _E |` A ) Part A ) : No typesetting found for wff ( MembPart A <-> ( `' _E |` A ) Part A ) with typecode wff