Metamath Proof Explorer


Definition df-coels

Description: Define the class of coelements on the class A , see also the alternate definition dfcoels . Possible definitions are the special cases of dfcoss3 and dfcoss4 . (Contributed by Peter Mazsa, 20-Nov-2019)

Ref Expression
Assertion df-coels 𝐴 = ≀ ( E ↾ 𝐴 )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 𝐴
1 0 ccoels 𝐴
2 cep E
3 2 ccnv E
4 3 0 cres ( E ↾ 𝐴 )
5 4 ccoss ≀ ( E ↾ 𝐴 )
6 1 5 wceq 𝐴 = ≀ ( E ↾ 𝐴 )