Definition df-coels 39097

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39115. Possible definitions are the special cases of dfcoss3 39099 and dfcoss4 39100. (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 38779	. 2 class ∼ 𝐴
3		cep 5560	. . . . 5 class E
4	3	ccnv 5660	. . . 4 class ◡ E
5	4, 1	cres 5663	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38778	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1568	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  39109  dfcoels  39115  dmcoels  39142  dfcoeleqvrels  39300  dfcoeleqvrel  39301  dmqs1cosscnvepreseq  39342  dfcomember  39352  eqvreldmqs2  39356  eldisjim2  39483  eldisjlem19  39508