Definition df-membparts 39770

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 39125	. 2 class MembParts
2		cep 5550	. . . . . 6 class E
3	2	ccnv 5650	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1569	. . . . 5 class 𝑎
6	3, 5	cres 5653	. . . 4 class (◡ E ↾ 𝑎)
7		cparts 39123	. . . 4 class Parts
8	6, 5, 7	wbr 5103	. . 3 wff (◡ E ↾ 𝑎) Parts 𝑎
9	8, 4	cab 2739	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}
10	1, 9	wceq 1570	1 wff MembParts = {𝑎 ∣ (◡ E ↾ 𝑎) Parts 𝑎}

This definition is used by:  mpets  39856