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

Metamath Proof Explorer

Theorem eldisjim2

Description: Alternate form of eldisjim . (Contributed by Peter Mazsa, 30-Dec-2024)

Ref Expression
Assertion eldisjim2 ⊢ ElDisj A → EqvRel ∼ A

Proof

Step Hyp Ref Expression
1 disjim ⊢ Disj E -1 ↾ A → EqvRel ≀ E -1 ↾ A
2 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
3 df-coels ⊢ ∼ A = ≀ E -1 ↾ A
4 3 eqvreleqi ⊢ EqvRel ∼ A ↔ EqvRel ≀ E -1 ↾ A
5 1 2 4 3imtr4i ⊢ ElDisj A → EqvRel ∼ A