Definition df-coels 38410

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38428. Possible definitions are the special cases of dfcoss3 38412 and dfcoss4 38413. (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 38177	. 2 class ∼ 𝐴
3		cep 5540	. . . . 5 class E
4	3	ccnv 5640	. . . 4 class ◡ E
5	4, 1	cres 5643	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38176	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38422  dfcoels  38428  dmcoels  38455  dfcoeleqvrels  38619  dfcoeleqvrel  38620  dmqs1cosscnvepreseq  38661  dfcomember  38671  eqvreldmqs2  38675  eldisjim2  38784  eldisjlem19  38809