Definition df-coels 38409

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38427. Possible definitions are the special cases of dfcoss3 38411 and dfcoss4 38412. (Contributed by Peter Mazsa, 20-Nov-2019.)

Assertion

Ref	Expression
df-coels	⊢ ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

Detailed syntax breakdown of Definition df-coels

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	ccoels 38176	. 2 class ∼ 𝐴
3		cep 5518	. . . . 5 class E
4	3	ccnv 5618	. . . 4 class ◡ E
5	4, 1	cres 5621	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38175	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38421  dfcoels  38427  dmcoels  38454  dfcoeleqvrels  38618  dfcoeleqvrel  38619  dmqs1cosscnvepreseq  38660  dfcomember  38670  eqvreldmqs2  38674  eldisjim2  38783  eldisjlem19  38808