Definition df-coels 38811

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38829. Possible definitions are the special cases of dfcoss3 38813 and dfcoss4 38814. (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 38493	. 2 class ∼ 𝐴
3		cep 5519	. . . . 5 class E
4	3	ccnv 5619	. . . 4 class ◡ E
5	4, 1	cres 5622	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38492	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1542	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38823  dfcoels  38829  dmcoels  38856  dfcoeleqvrels  39014  dfcoeleqvrel  39015  dmqs1cosscnvepreseq  39056  dfcomember  39066  eqvreldmqs2  39070  eldisjim2  39197  eldisjlem19  39222