Definition df-membparts

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmembparts	⊢ MembParts
1		va	⊢ 𝑎
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	1	cv	⊢ 𝑎
5	3 4	cres	⊢ ( ◡ E ↾ 𝑎 )
6		cparts	⊢ Parts
7	5 4 6	wbr	⊢ ( ◡ E ↾ 𝑎 ) Parts 𝑎
8	7 1	cab	⊢ { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) Parts 𝑎 }
9	0 8	wceq	⊢ MembParts = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) Parts 𝑎 }