Definition df-coels 39179

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 39197. Possible definitions are the special cases of dfcoss3 39181 and dfcoss4 39182. (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 38861	. 2 class ∼ 𝐴
3		cep 5559	. . . . 5 class E
4	3	ccnv 5659	. . . 4 class ◡ E
5	4, 1	cres 5662	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 38860	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1569	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is used by:  relcoels  39191  dfcoels  39197  dmcoels  39224  dfcoeleqvrels  39382  dfcoeleqvrel  39383  dmqs1cosscnvepreseq  39424  dfcomember  39434  eqvreldmqs2  39438  eldisjim2  39565  eldisjlem19  39590