Definition df-coels 38672

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38690. Possible definitions are the special cases of dfcoss3 38674 and dfcoss4 38675. (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 38354	. 2 class ∼ 𝐴
3		cep 5522	. . . . 5 class E
4	3	ccnv 5622	. . . 4 class ◡ E
5	4, 1	cres 5625	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38353	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1542	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38684  dfcoels  38690  dmcoels  38717  dfcoeleqvrels  38875  dfcoeleqvrel  38876  dmqs1cosscnvepreseq  38917  dfcomember  38927  eqvreldmqs2  38931  eldisjim2  39058  eldisjlem19  39083