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 35768
Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 35783. Possible definitions are the special cases of dfcoss3 35770 and dfcoss4 35771. (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 35562 . 2 class 𝐴
3 cep 5451 . . . . 5 class E
43ccnv 5541 . . . 4 class E
54, 1cres 5544 . . 3 class ( E ↾ 𝐴)
65ccoss 35561 . 2 class ≀ ( E ↾ 𝐴)
72, 6wceq 1538 1 wff 𝐴 = ≀ ( E ↾ 𝐴)
Colors of variables: wff setvar class
This definition is referenced by:  relcoels  35777  dfcoels  35783  dmcoels  35805  dfcoeleqvrels  35964  dfcoeleqvrel  35965  dmqs1cosscnvepreseq  36004  dfmember  36014
  Copyright terms: Public domain W3C validator