This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-comembers

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)

		Ref	Expression
	Assertion	df-comembers	$⊢ CoMembErs = \{a \| ≀ ({E^{-1} ↾}_{a}) Ers a\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccomembers	$class CoMembErs$
1		va	$setvar a$
2		cep	$class E$
3	2	ccnv	$class E^{-1}$
4	1	cv	$setvar a$
5	3 4	cres	$class ({E^{-1} ↾}_{a})$
6	5	ccoss	$class ≀ ({E^{-1} ↾}_{a})$
7		cers	$class Ers$
8	6 4 7	wbr	$wff ≀ ({E^{-1} ↾}_{a}) Ers a$
9	8 1	cab	$class \{a \| ≀ ({E^{-1} ↾}_{a}) Ers a\}$
10	0 9	wceq	$wff CoMembErs = \{a \| ≀ ({E^{-1} ↾}_{a}) Ers a\}$