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