Definition df-coels 38413

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38431. Possible definitions are the special cases of dfcoss3 38415 and dfcoss4 38416. (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 38183	. 2 class ∼ 𝐴
3		cep 5583	. . . . 5 class E
4	3	ccnv 5684	. . . 4 class ◡ E
5	4, 1	cres 5687	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38182	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38425  dfcoels  38431  dmcoels  38458  dfcoeleqvrels  38622  dfcoeleqvrel  38623  dmqs1cosscnvepreseq  38663  dfcomember  38673  eqvreldmqs2  38677  eldisjim2  38786  eldisjlem19  38811