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 38413
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.)
Assertion
Ref Expression
df-coels 𝐴 = ≀ ( E ↾ 𝐴)

Detailed syntax breakdown of Definition df-coels
StepHypRef Expression
1 cA . . 3 class 𝐴
21ccoels 38183 . 2 class 𝐴
3 cep 5583 . . . . 5 class E
43ccnv 5684 . . . 4 class E
54, 1cres 5687 . . 3 class ( E ↾ 𝐴)
65ccoss 38182 . 2 class ≀ ( E ↾ 𝐴)
72, 6wceq 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