Definition df-coels 39626

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39644. Possible definitions are the special cases of dfcoss3 39628 and dfcoss4 39629. (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 39308	. 2 class ∼ 𝐴
3		cep 5554	. . . . 5 class E
4	3	ccnv 5654	. . . 4 class ◡ E
5	4, 1	cres 5657	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 39307	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1570	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is used by:  relcoels  39638  dfcoels  39644  dmcoels  39671  dfcoeleqvrels  39829  dfcoeleqvrel  39830  dmqs1cosscnvepreseq  39871  dfcomember  39881  eqvreldmqs2  39885  eldisjim2  40012  eldisjlem19  40037