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 = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmembers	⊢ MembErs
1		va	⊢ 𝑎
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	1	cv	⊢ 𝑎
5	3 4	cres	⊢ ( ◡ E ↾ 𝑎 )
6	5	ccoss	⊢ ≀ ( ◡ E ↾ 𝑎 )
7		cers	⊢ Ers
8	6 4 7	wbr	⊢ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎
9	8 1	cab	⊢ { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎 }
10	0 9	wceq	⊢ MembErs = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) Ers 𝑎 }