Metamath Proof Explorer

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 = a | ≀ E -1 ↾ a ∈ EqvRels

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccoeleqvrels class CoElEqvRels
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 ceqvrels class EqvRels
8 6 7 wcel wff ≀ E -1 ↾ a ∈ EqvRels
9 8 1 cab class a | ≀ E -1 ↾ a ∈ EqvRels
10 0 9 wceq wff CoElEqvRels = a | ≀ E -1 ↾ a ∈ EqvRels