Definition df-membparts 39560

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 38915	. 2 class MembParts
2		cep 5565	. . . . . 6 class E
3	2	ccnv 5665	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1569	. . . . 5 class 𝑎
6	3, 5	cres 5668	. . . 4 class (◡ E ↾ 𝑎)
7		cparts 38913	. . . 4 class Parts
8	6, 5, 7	wbr 5114	. . 3 wff (◡ E ↾ 𝑎) Parts 𝑎
9	8, 4	cab 2744	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
10	1, 9	wceq 1570	1 wff MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}

This definition is used by:  mpets  39646