Definition df-coels 38397

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38415. Possible definitions are the special cases of dfcoss3 38399 and dfcoss4 38400. (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 38164	. 2 class ∼ 𝐴
3		cep 5530	. . . . 5 class E
4	3	ccnv 5630	. . . 4 class ◡ E
5	4, 1	cres 5633	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38163	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38409  dfcoels  38415  dmcoels  38442  dfcoeleqvrels  38606  dfcoeleqvrel  38607  dmqs1cosscnvepreseq  38648  dfcomember  38658  eqvreldmqs2  38662  eldisjim2  38771  eldisjlem19  38796