Definition df-coels 38394

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38412. Possible definitions are the special cases of dfcoss3 38396 and dfcoss4 38397. (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 38163	. 2 class ∼ 𝐴
3		cep 5588	. . . . 5 class E
4	3	ccnv 5688	. . . 4 class ◡ E
5	4, 1	cres 5691	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38162	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1537	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38406  dfcoels  38412  dmcoels  38439  dfcoeleqvrels  38603  dfcoeleqvrel  38604  dmqs1cosscnvepreseq  38644  dfcomember  38654  eqvreldmqs2  38658  eldisjim2  38767  eldisjlem19  38792