Definition df-comembers 37530

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

Assertion

Ref	Expression
df-comembers	⊢ CoMembErs = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) Ers 𝑎}

Detailed syntax breakdown of Definition df-comembers

Step	Hyp	Ref	Expression
1		ccomembers 37065	. 2 class CoMembErs
2		cep 5579	. . . . . . 7 class E
3	2	ccnv 5675	. . . . . 6 class ◡ E
4		va	. . . . . . 7 setvar 𝑎
5	4	cv 1540	. . . . . 6 class 𝑎
6	3, 5	cres 5678	. . . . 5 class (◡ E ↾ 𝑎)
7	6	ccoss 37038	. . . 4 class ≀ (◡ E ↾ 𝑎)
8		cers 37063	. . . 4 class Ers
9	7, 5, 8	wbr 5148	. . 3 wff ≀ (◡ E ↾ 𝑎) Ers 𝑎
10	9, 4	cab 2709	. 2 class {𝑎 ∣ ≀ (◡ E ↾ 𝑎) Ers 𝑎}
11	1, 10	wceq 1541	1 wff CoMembErs = {𝑎 ∣ ≀ (◡ E ↾ 𝑎) Ers 𝑎}

This definition is referenced by:  mpets  37707