Definition df-coels 36465

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 36480. Possible definitions are the special cases of dfcoss3 36467 and dfcoss4 36468. (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 36261	. 2 class ∼ 𝐴
3		cep 5485	. . . . 5 class E
4	3	ccnv 5579	. . . 4 class ◡ E
5	4, 1	cres 5582	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 36260	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1539	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  36474  dfcoels  36480  dmcoels  36502  dfcoeleqvrels  36661  dfcoeleqvrel  36662  dmqs1cosscnvepreseq  36701  dfmember  36711