Definition df-membpart 39803

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 39805.

Member partition is the conventional meaning of partition (see the notes of df-parts 39800 and dfmembpart2 39805), we generalize the concept in df-parts 39800 and df-part 39801.

Member partition and comember equivalence are the same by mpet 39885. (Contributed by Peter Mazsa, 26-Jun-2021.)

Assertion

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

Detailed syntax breakdown of Definition df-membpart

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wmembpart 39158	. 2 wff MembPart 𝐴
3		cep 5550	. . . . 5 class E
4	3	ccnv 5650	. . . 4 class ◡ E
5	4, 1	cres 5653	. . 3 class (◡ E ↾ 𝐴)
6	1, 5	wpart 39156	. 2 wff (◡ E ↾ 𝐴) Part 𝐴
7	2, 6	wb 209	1 wff ( MembPart 𝐴 ↔ (◡ E ↾ 𝐴) Part 𝐴)

This definition is used by:  dfmembpart2  39805  mpet2  39886