Definition df-coels 39354

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39372. Possible definitions are the special cases of dfcoss3 39356 and dfcoss4 39357. (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 39036	. 2 class ∼ 𝐴
3		cep 5546	. . . . 5 class E
4	3	ccnv 5646	. . . 4 class ◡ E
5	4, 1	cres 5649	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 39035	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1570	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is used by:  relcoels  39366  dfcoels  39372  dmcoels  39399  dfcoeleqvrels  39557  dfcoeleqvrel  39558  dmqs1cosscnvepreseq  39599  dfcomember  39609  eqvreldmqs2  39613  eldisjim2  39740  eldisjlem19  39765