Definition df-coels 38716

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38734. Possible definitions are the special cases of dfcoss3 38718 and dfcoss4 38719. (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 38398	. 2 class ∼ 𝐴
3		cep 5524	. . . . 5 class E
4	3	ccnv 5624	. . . 4 class ◡ E
5	4, 1	cres 5627	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38397	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1542	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38728  dfcoels  38734  dmcoels  38761  dfcoeleqvrels  38919  dfcoeleqvrel  38920  dmqs1cosscnvepreseq  38961  dfcomember  38971  eqvreldmqs2  38975  eldisjim2  39102  eldisjlem19  39127