Definition df-coels 35692

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 35707. Possible definitions are the special cases of dfcoss3 35694 and dfcoss4 35695. (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 35486	. 2 class ∼ 𝐴
3		cep 5450	. . . . 5 class E
4	3	ccnv 5540	. . . 4 class ◡ E
5	4, 1	cres 5543	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 35485	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1537	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  35701  dfcoels  35707  dmcoels  35729  dfcoeleqvrels  35888  dfcoeleqvrel  35889  dmqs1cosscnvepreseq  35928  dfmember  35938