Definition df-coels 39006

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39024. Possible definitions are the special cases of dfcoss3 39008 and dfcoss4 39009. (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 38688	. 2 class ∼ 𝐴
3		cep 5548	. . . . 5 class E
4	3	ccnv 5648	. . . 4 class ◡ E
5	4, 1	cres 5651	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38687	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1562	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  39018  dfcoels  39024  dmcoels  39051  dfcoeleqvrels  39209  dfcoeleqvrel  39210  dmqs1cosscnvepreseq  39251  dfcomember  39261  eqvreldmqs2  39265  eldisjim2  39392  eldisjlem19  39417