Definition df-coels 38396

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 38414. Possible definitions are the special cases of dfcoss3 38398 and dfcoss4 38399. (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 38163	. 2 class ∼ 𝐴
3		cep 5530	. . . . 5 class E
4	3	ccnv 5630	. . . 4 class ◡ E
5	4, 1	cres 5633	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38162	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1540	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  38408  dfcoels  38414  dmcoels  38441  dfcoeleqvrels  38605  dfcoeleqvrel  38606  dmqs1cosscnvepreseq  38647  dfcomember  38657  eqvreldmqs2  38661  eldisjim2  38770  eldisjlem19  38795