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

Definition df-coels 34664
Description: Define the class of coelements on the class 𝐴, cf. the alternate definition dfcoels 34679. Possible definitions are the special cases of dfcoss3 34666 and dfcoss4 34667. (Contributed by Peter Mazsa, 20-Nov-2019.)
Assertion
Ref Expression
df-coels 𝐴 = ≀ ( E ↾ 𝐴)

Detailed syntax breakdown of Definition df-coels
StepHypRef Expression
1 cA . . 3 class 𝐴
21ccoels 34470 . 2 class 𝐴
3 cep 5224 . . . . 5 class E
43ccnv 5311 . . . 4 class E
54, 1cres 5314 . . 3 class ( E ↾ 𝐴)
65ccoss 34469 . 2 class ≀ ( E ↾ 𝐴)
72, 6wceq 1653 1 wff 𝐴 = ≀ ( E ↾ 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  relcoels  34673  dfcoels  34679  dmcoels  34701  eqvrelcoels4  34856
  Copyright terms: Public domain W3C validator