Definition df-coels 39510

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39528. Possible definitions are the special cases of dfcoss3 39512 and dfcoss4 39513. (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 39192	. 2 class ∼ 𝐴
3		cep 5549	. . . . 5 class E
4	3	ccnv 5649	. . . 4 class ◡ E
5	4, 1	cres 5652	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 39191	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1569	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is used by:  relcoels  39522  dfcoels  39528  dmcoels  39555  dfcoeleqvrels  39713  dfcoeleqvrel  39714  dmqs1cosscnvepreseq  39755  dfcomember  39765  eqvreldmqs2  39769  eldisjim2  39896  eldisjlem19  39921