Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-membpart Structured version   Visualization version   GIF version

Definition df-membpart 37161
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.)

Assertion
Ref Expression
df-membpart ( MembPart 𝐴 ↔ ( E ↾ 𝐴) Part 𝐴)

Detailed syntax breakdown of Definition df-membpart
StepHypRef Expression
1 cA . . 3 class 𝐴
21wmembpart 36606 . 2 wff MembPart 𝐴
3 cep 5534 . . . . 5 class E
43ccnv 5630 . . . 4 class E
54, 1cres 5633 . . 3 class ( E ↾ 𝐴)
61, 5wpart 36604 . 2 wff ( E ↾ 𝐴) Part 𝐴
72, 6wb 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