Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-coeleqvrels Structured version   Visualization version   GIF version

Definition df-coeleqvrels 38587
Description: Define 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 38597. Alternate definition is dfcoeleqvrels 38622. (Contributed by Peter Mazsa, 28-Nov-2022.)
Assertion
Ref Expression
df-coeleqvrels CoElEqvRels = {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }

Detailed syntax breakdown of Definition df-coeleqvrels
StepHypRef Expression
1 ccoeleqvrels 38200 . 2 class CoElEqvRels
2 cep 5583 . . . . . . 7 class E
32ccnv 5684 . . . . . 6 class E
4 va . . . . . . 7 setvar 𝑎
54cv 1539 . . . . . 6 class 𝑎
63, 5cres 5687 . . . . 5 class ( E ↾ 𝑎)
76ccoss 38182 . . . 4 class ≀ ( E ↾ 𝑎)
8 ceqvrels 38198 . . . 4 class EqvRels
97, 8wcel 2108 . . 3 wff ≀ ( E ↾ 𝑎) ∈ EqvRels
109, 4cab 2714 . 2 class {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }
111, 10wceq 1540 1 wff CoElEqvRels = {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }
Colors of variables: wff setvar class
This definition is referenced by:  elcoeleqvrels  38596  dfcoeleqvrels  38622
  Copyright terms: Public domain W3C validator