Definition df-coels 36841

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 36859. Possible definitions are the special cases of dfcoss3 36843 and dfcoss4 36844. (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 36602	. 2 class ∼ 𝐴
3		cep 5534	. . . . 5 class E
4	3	ccnv 5630	. . . 4 class ◡ E
5	4, 1	cres 5633	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 36601	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1541	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  36853  dfcoels  36859  dmcoels  36886  dfcoeleqvrels  37050  dfcoeleqvrel  37051  dmqs1cosscnvepreseq  37091  dfcomember  37101  eqvreldmqs2  37105  eldisjim2  37214  eldisjlem19  37239