| Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-coels | Structured version Visualization version GIF version | ||
| Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38431. Possible definitions are the special cases of dfcoss3 38415 and dfcoss4 38416. (Contributed by Peter Mazsa, 20-Nov-2019.) |
| Ref | Expression |
|---|---|
| df-coels | ⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | 1 | ccoels 38183 | . 2 class ∼ 𝐴 |
| 3 | cep 5583 | . . . . 5 class E | |
| 4 | 3 | ccnv 5684 | . . . 4 class ◡ E |
| 5 | 4, 1 | cres 5687 | . . 3 class (◡ E ↾ 𝐴) |
| 6 | 5 | ccoss 38182 | . 2 class ≀ (◡ E ↾ 𝐴) |
| 7 | 2, 6 | wceq 1540 | 1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴) |
| Colors of variables: wff setvar class |
| This definition is referenced by: relcoels 38425 dfcoels 38431 dmcoels 38458 dfcoeleqvrels 38622 dfcoeleqvrel 38623 dmqs1cosscnvepreseq 38663 dfcomember 38673 eqvreldmqs2 38677 eldisjim2 38786 eldisjlem19 38811 |
| Copyright terms: Public domain | W3C validator |