Definition df-coels 38820

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38838. Possible definitions are the special cases of dfcoss3 38822 and dfcoss4 38823. (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 38502	. 2 class ∼ 𝐴
3		cep 5527	. . . . 5 class E
4	3	ccnv 5627	. . . 4 class ◡ E
5	4, 1	cres 5630	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38501	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1542	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38832  dfcoels  38838  dmcoels  38865  dfcoeleqvrels  39023  dfcoeleqvrel  39024  dmqs1cosscnvepreseq  39065  dfcomember  39075  eqvreldmqs2  39079  eldisjim2  39206  eldisjlem19  39231