Definition df-coels 37277

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 37295. Possible definitions are the special cases of dfcoss3 37279 and dfcoss4 37280. (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 37039	. 2 class ∼ 𝐴
3		cep 5579	. . . . 5 class E
4	3	ccnv 5675	. . . 4 class ◡ E
5	4, 1	cres 5678	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 37038	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1541	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  37289  dfcoels  37295  dmcoels  37322  dfcoeleqvrels  37486  dfcoeleqvrel  37487  dmqs1cosscnvepreseq  37527  dfcomember  37537  eqvreldmqs2  37541  eldisjim2  37650  eldisjlem19  37675