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 38542
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 38552. Alternate definition is dfcoeleqvrels 38577. (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 38153 . 2 class CoElEqvRels
2 cep 5598 . . . . . . 7 class E
32ccnv 5699 . . . . . 6 class E
4 va . . . . . . 7 setvar 𝑎
54cv 1536 . . . . . 6 class 𝑎
63, 5cres 5702 . . . . 5 class ( E ↾ 𝑎)
76ccoss 38135 . . . 4 class ≀ ( E ↾ 𝑎)
8 ceqvrels 38151 . . . 4 class EqvRels
97, 8wcel 2108 . . 3 wff ≀ ( E ↾ 𝑎) ∈ EqvRels
109, 4cab 2717 . 2 class {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }
111, 10wceq 1537 1 wff CoElEqvRels = {𝑎 ∣ ≀ ( E ↾ 𝑎) ∈ EqvRels }
Colors of variables: wff setvar class
This definition is referenced by:  elcoeleqvrels  38551  dfcoeleqvrels  38577
  Copyright terms: Public domain W3C validator