Definition df-coels 38882

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38900. Possible definitions are the special cases of dfcoss3 38884 and dfcoss4 38885. (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 38564	. 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 38563	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1548	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38894  dfcoels  38900  dmcoels  38927  dfcoeleqvrels  39085  dfcoeleqvrel  39086  dmqs1cosscnvepreseq  39127  dfcomember  39137  eqvreldmqs2  39141  eldisjim2  39268  eldisjlem19  39293