Definition df-membparts 36981

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 36421	. 2 class MembParts
2		cep 5505	. . . . . 6 class E
3	2	ccnv 5599	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1538	. . . . 5 class 𝑎
6	3, 5	cres 5602	. . . 4 class (◡ E ↾ 𝑎)
7		cparts 36419	. . . 4 class Parts
8	6, 5, 7	wbr 5081	. . 3 wff (◡ E ↾ 𝑎) Parts 𝑎
9	8, 4	cab 2713	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
10	1, 9	wceq 1539	1 wff MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}

This definition is referenced by:  mpets  37056