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	Could not format assertion : No typesetting found for |- MembParts = { a | ( `' _E |` a ) Parts a } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmembparts	Could not format MembParts : No typesetting found for class MembParts with typecode class
1		va	$$setvara$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	1	cv	$$setvara$$
5	3 4	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
6		cparts	Could not format Parts : No typesetting found for class Parts with typecode class
7	5 4 6	wbr	Could not format ( `' _E |` a ) Parts a : No typesetting found for wff ( `' _E |` a ) Parts a with typecode wff
8	7 1	cab	Could not format { a | ( `' _E |` a ) Parts a } : No typesetting found for class { a | ( `' _E |` a ) Parts a } with typecode class
9	0 8	wceq	Could not format MembParts = { a | ( `' _E |` a ) Parts a } : No typesetting found for wff MembParts = { a | ( `' _E |` a ) Parts a } with typecode wff