Definition df-coels 39252

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39270. Possible definitions are the special cases of dfcoss3 39254 and dfcoss4 39255. (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 38934	. 2 class ∼ 𝐴
3		cep 5558	. . . . 5 class E
4	3	ccnv 5658	. . . 4 class ◡ E
5	4, 1	cres 5661	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38933	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1570	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is used by:  relcoels  39264  dfcoels  39270  dmcoels  39297  dfcoeleqvrels  39455  dfcoeleqvrel  39456  dmqs1cosscnvepreseq  39497  dfcomember  39507  eqvreldmqs2  39511  eldisjim2  39638  eldisjlem19  39663