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

Metamath Proof Explorer

Theorem relcoels

Description: Coelements on A is a relation. (Contributed by Peter Mazsa, 5-Oct-2021)

Ref Expression
Assertion relcoels ⊢ Rel ⁡ ∼ A

Proof

Step Hyp Ref Expression
1 relcoss ⊢ Rel ⁡ ≀ E -1 ↾ A
2 df-coels ⊢ ∼ A = ≀ E -1 ↾ A
3 2 releqi ⊢ Rel ⁡ ∼ A ↔ Rel ⁡ ≀ E -1 ↾ A
4 1 3 mpbir ⊢ Rel ⁡ ∼ A