Definition df-coeleqvrels

Description: Define the the coelement equivalence relations class, the class of sets with coelement equivalence relations. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel . Alternate definition is dfcoeleqvrels . (Contributed by Peter Mazsa, 28-Nov-2022)

	Ref	Expression
Assertion	df-coeleqvrels	⊢ CoElEqvRels = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccoeleqvrels	⊢ CoElEqvRels
1		va	⊢ 𝑎
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	1	cv	⊢ 𝑎
5	3 4	cres	⊢ ( ◡ E ↾ 𝑎 )
6	5	ccoss	⊢ ≀ ( ◡ E ↾ 𝑎 )
7		ceqvrels	⊢ EqvRels
8	6 7	wcel	⊢ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels
9	8 1	cab	⊢ { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels }
10	0 9	wceq	⊢ CoElEqvRels = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels }