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 38568
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 38578. Alternate definition is dfcoeleqvrels 38603. (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 38180 . 2 class CoElEqvRels
2 cep 5588 . . . . . . 7 class E
32ccnv 5688 . . . . . 6 class E
4 va . . . . . . 7 setvar 𝑎
54cv 1536 . . . . . 6 class 𝑎
63, 5cres 5691 . . . . 5 class ( E ↾ 𝑎)
76ccoss 38162 . . . 4 class ≀ ( E ↾ 𝑎)
8 ceqvrels 38178 . . . 4 class EqvRels
97, 8wcel 2106 . . 3 wff ≀ ( E ↾ 𝑎) ∈ EqvRels
109, 4cab 2712 . 2 class {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }
111, 10wceq 1537 1 wff CoElEqvRels = {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }
Colors of variables: wff setvar class
This definition is referenced by:  elcoeleqvrels  38577  dfcoeleqvrels  38603
  Copyright terms: Public domain W3C validator