Definition df-coels 38368

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38386. Possible definitions are the special cases of dfcoss3 38370 and dfcoss4 38371. (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 38136	. 2 class ∼ 𝐴
3		cep 5598	. . . . 5 class E
4	3	ccnv 5699	. . . 4 class ◡ E
5	4, 1	cres 5702	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38135	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1537	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38380  dfcoels  38386  dmcoels  38413  dfcoeleqvrels  38577  dfcoeleqvrel  38578  dmqs1cosscnvepreseq  38618  dfcomember  38628  eqvreldmqs2  38632  eldisjim2  38741  eldisjlem19  38766