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 | |- ( MembPart A <-> ( `' _E |` A ) Part A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | wmembpart | |- MembPart A |
| 2 | cep | |- _E |
|
| 3 | 2 | ccnv | |- `' _E |
| 4 | 3 0 | cres | |- ( `' _E |` A ) |
| 5 | 0 4 | wpart | |- ( `' _E |` A ) Part A |
| 6 | 1 5 | wb | |- ( MembPart A <-> ( `' _E |` A ) Part A ) |