Theorem eldisjim2

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

	Ref	Expression
Assertion	eldisjim2	⊢ ( ElDisj 𝐴 → EqvRel ∼ 𝐴 )

Proof

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