Definition df-coels 38814

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38832. Possible definitions are the special cases of dfcoss3 38816 and dfcoss4 38817. (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 38496	. 2 class ∼ 𝐴
3		cep 5521	. . . . 5 class E
4	3	ccnv 5621	. . . 4 class ◡ E
5	4, 1	cres 5624	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38495	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1542	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38826  dfcoels  38832  dmcoels  38859  dfcoeleqvrels  39017  dfcoeleqvrel  39018  dmqs1cosscnvepreseq  39059  dfcomember  39069  eqvreldmqs2  39073  eldisjim2  39200  eldisjlem19  39225