Definition df-membparts 38748

Description: Define the class of member partition relations on their domain quotients. (Contributed by Peter Mazsa, 26-Jun-2021.)

Assertion

Ref	Expression
df-membparts	⊢ MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}

Detailed syntax breakdown of Definition df-membparts

Step	Hyp	Ref	Expression
1		cmembparts 38201	. 2 class MembParts
2		cep 5587	. . . . . 6 class E
3	2	ccnv 5687	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1535	. . . . 5 class 𝑎
6	3, 5	cres 5690	. . . 4 class (◡ E ↾ 𝑎)
7		cparts 38199	. . . 4 class Parts
8	6, 5, 7	wbr 5147	. . 3 wff (◡ E ↾ 𝑎) Parts 𝑎
9	8, 4	cab 2711	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
10	1, 9	wceq 1536	1 wff MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}

This definition is referenced by:  mpets  38823