Definition df-coels 39435

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39453. Possible definitions are the special cases of dfcoss3 39437 and dfcoss4 39438. (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 39117	. 2 class ∼ 𝐴
3		cep 5549	. . . . 5 class E
4	3	ccnv 5649	. . . 4 class ◡ E
5	4, 1	cres 5652	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 39116	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1569	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is used by:  relcoels  39447  dfcoels  39453  dmcoels  39480  dfcoeleqvrels  39638  dfcoeleqvrel  39639  dmqs1cosscnvepreseq  39680  dfcomember  39690  eqvreldmqs2  39694  eldisjim2  39821  eldisjlem19  39846