![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-membpart | Structured version Visualization version GIF version |
Description: Define the member
partition predicate, or the disjoint restricted element
relation on its domain quotient predicate. (Read: 𝐴 is a member
partition.) A alternative definition is dfmembpart2 37163.
Member partition is the conventional meaning of partition (see the notes of df-parts 37158 and dfmembpart2 37163), we generalize the concept in df-parts 37158 and df-part 37159. Member partition and comember equivalence are the same by mpet 37232. (Contributed by Peter Mazsa, 26-Jun-2021.) |
Ref | Expression |
---|---|
df-membpart | ⊢ ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wmembpart 36606 | . 2 wff MembPart 𝐴 |
3 | cep 5534 | . . . . 5 class E | |
4 | 3 | ccnv 5630 | . . . 4 class ◡ E |
5 | 4, 1 | cres 5633 | . . 3 class (◡ E ↾ 𝐴) |
6 | 1, 5 | wpart 36604 | . 2 wff (◡ E ↾ 𝐴) Part 𝐴 |
7 | 2, 6 | wb 205 | 1 wff ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴) |
Colors of variables: wff setvar class |
This definition is referenced by: dfmembpart2 37163 mpet2 37233 |
Copyright terms: Public domain | W3C validator |