![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-coeleqvrel | Structured version Visualization version GIF version |
Description: Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on 𝐴.) Alternate definition is dfcoeleqvrel 37584. For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel 37558. (Contributed by Peter Mazsa, 11-Dec-2021.) |
Ref | Expression |
---|---|
df-coeleqvrel | ⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wcoeleqvrel 37154 | . 2 wff CoElEqvRel 𝐴 |
3 | cep 5579 | . . . . . 6 class E | |
4 | 3 | ccnv 5675 | . . . . 5 class ◡ E |
5 | 4, 1 | cres 5678 | . . . 4 class (◡ E ↾ 𝐴) |
6 | 5 | ccoss 37135 | . . 3 class ≀ (◡ E ↾ 𝐴) |
7 | 6 | weqvrel 37152 | . 2 wff EqvRel ≀ (◡ E ↾ 𝐴) |
8 | 2, 7 | wb 205 | 1 wff ( CoElEqvRel 𝐴 ↔ EqvRel ≀ (◡ E ↾ 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: elcoeleqvrelsrel 37558 dfcoeleqvrel 37584 eqvreldmqs 37637 eldisjim 37746 |
Copyright terms: Public domain | W3C validator |