This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∼ A = ≀ E -1 ↾ A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 ccoels class ∼ A
2 cep class E
3 2 ccnv class E -1
4 3 0 cres class E -1 ↾ A
5 4 ccoss class ≀ E -1 ↾ A
6 1 5 wceq wff ∼ A = ≀ E -1 ↾ A