Definition df-membparts 38768

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 38222	. 2 class MembParts
2		cep 5583	. . . . . 6 class E
3	2	ccnv 5684	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1539	. . . . 5 class 𝑎
6	3, 5	cres 5687	. . . 4 class (◡ E ↾ 𝑎)
7		cparts 38220	. . . 4 class Parts
8	6, 5, 7	wbr 5143	. . 3 wff (◡ E ↾ 𝑎) Parts 𝑎
9	8, 4	cab 2714	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
10	1, 9	wceq 1540	1 wff MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}

This definition is referenced by:  mpets  38843