Definition df-coels 38430

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38448. Possible definitions are the special cases of dfcoss3 38432 and dfcoss4 38433. (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 38200	. 2 class ∼ 𝐴
3		cep 5552	. . . . 5 class E
4	3	ccnv 5653	. . . 4 class ◡ E
5	4, 1	cres 5656	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38199	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38442  dfcoels  38448  dmcoels  38475  dfcoeleqvrels  38639  dfcoeleqvrel  38640  dmqs1cosscnvepreseq  38680  dfcomember  38690  eqvreldmqs2  38694  eldisjim2  38803  eldisjlem19  38828