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 |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cA | ||
1 | 0 | wmembpart | Could not format MembPart A : No typesetting found for wff MembPart A with typecode wff |
2 | cep | ||
3 | 2 | ccnv | |
4 | 3 0 | cres | |
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 |