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 ↾ 𝐴 ) |
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 ↾ 𝐴 ) |