Definition df-coels 38403

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38421. Possible definitions are the special cases of dfcoss3 38405 and dfcoss4 38406. (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 38170	. 2 class ∼ 𝐴
3		cep 5537	. . . . 5 class E
4	3	ccnv 5637	. . . 4 class ◡ E
5	4, 1	cres 5640	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38169	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38415  dfcoels  38421  dmcoels  38448  dfcoeleqvrels  38612  dfcoeleqvrel  38613  dmqs1cosscnvepreseq  38654  dfcomember  38664  eqvreldmqs2  38668  eldisjim2  38777  eldisjlem19  38802