Definition df-members

Description: Define the class of membership equivalence relations on their domain quotients. (Contributed by Peter Mazsa, 28-Nov-2022) (Revised by Peter Mazsa, 24-Jul-2023)

	Ref	Expression
Assertion	df-members	|- MembErs = { a | ,~ ( `' _E |` a ) Ers a }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmembers	|- MembErs
1		va	|- a
2		cep	|- _E
3	2	ccnv	|- `' _E
4	1	cv	|- a
5	3 4	cres	|- ( `' _E |` a )
6	5	ccoss	|- ,~ ( `' _E |` a )
7		cers	|- Ers
8	6 4 7	wbr	|- ,~ ( `' _E |` a ) Ers a
9	8 1	cab	|- { a | ,~ ( `' _E |` a ) Ers a }
10	0 9	wceq	|- MembErs = { a | ,~ ( `' _E |` a ) Ers a }