Definition df-coels 37585

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 37603. Possible definitions are the special cases of dfcoss3 37587 and dfcoss4 37588. (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 37347	. 2 class ∼ 𝐴
3		cep 5578	. . . . 5 class E
4	3	ccnv 5674	. . . 4 class ◡ E
5	4, 1	cres 5677	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 37346	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1539	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  37597  dfcoels  37603  dmcoels  37630  dfcoeleqvrels  37794  dfcoeleqvrel  37795  dmqs1cosscnvepreseq  37835  dfcomember  37845  eqvreldmqs2  37849  eldisjim2  37958  eldisjlem19  37983