Definition df-coels 38671

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38689. Possible definitions are the special cases of dfcoss3 38673 and dfcoss4 38674. (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 38380	. 2 class ∼ 𝐴
3		cep 5523	. . . . 5 class E
4	3	ccnv 5623	. . . 4 class ◡ E
5	4, 1	cres 5626	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38379	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1541	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38683  dfcoels  38689  dmcoels  38716  dfcoeleqvrels  38874  dfcoeleqvrel  38875  dmqs1cosscnvepreseq  38917  dfcomember  38927  eqvreldmqs2  38931  eldisjim2  39040  eldisjlem19  39065