Definition df-coels 34664

Description: Define the class of coelements on the class 𝐴, cf. the alternate definition dfcoels 34679. Possible definitions are the special cases of dfcoss3 34666 and dfcoss4 34667. (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 34470	. 2 class ∼ 𝐴
3		cep 5224	. . . . 5 class E
4	3	ccnv 5311	. . . 4 class ◡ E
5	4, 1	cres 5314	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 34469	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1653	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  34673  dfcoels  34679  dmcoels  34701  eqvrelcoels4  34856