Definition df-coels 35820

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 35835. Possible definitions are the special cases of dfcoss3 35822 and dfcoss4 35823. (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 35614	. 2 class ∼ 𝐴
3		cep 5429	. . . . 5 class E
4	3	ccnv 5518	. . . 4 class ◡ E
5	4, 1	cres 5521	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 35613	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1538	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  35829  dfcoels  35835  dmcoels  35857  dfcoeleqvrels  36016  dfcoeleqvrel  36017  dmqs1cosscnvepreseq  36056  dfmember  36066