Definition df-coels 38520

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38538. Possible definitions are the special cases of dfcoss3 38522 and dfcoss4 38523. (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 38229	. 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 38228	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1541	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38532  dfcoels  38538  dmcoels  38565  dfcoeleqvrels  38723  dfcoeleqvrel  38724  dmqs1cosscnvepreseq  38766  dfcomember  38776  eqvreldmqs2  38780  eldisjim2  38889  eldisjlem19  38914