Definition df-coels 36538

Description: Define the class of coelements on the class 𝐴, see also the alternate definition dfcoels 36553. Possible definitions are the special cases of dfcoss3 36540 and dfcoss4 36541. (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 36334	. 2 class ∼ 𝐴
3		cep 5494	. . . . 5 class E
4	3	ccnv 5588	. . . 4 class ◡ E
5	4, 1	cres 5591	. . 3 class (◡ E ↾ 𝐴)
6	5	ccoss 36333	. 2 class ≀ (◡ E ↾ 𝐴)
7	2, 6	wceq 1539	1 wff ∼ 𝐴 = ≀ (◡ E ↾ 𝐴)

This definition is referenced by:  relcoels  36547  dfcoels  36553  dmcoels  36575  dfcoeleqvrels  36734  dfcoeleqvrel  36735  dmqs1cosscnvepreseq  36774  dfmember  36784