Theorem eldisjim2

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

	Ref	Expression
Assertion	eldisjim2	$$⊢ElDisjA\to EqvRel\sim A$$

Proof

Step	Hyp	Ref	Expression
1		disjim	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\to EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3		df-coels	$$⊢\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
4	3	eqvreleqi	$$⊢EqvRel\sim A\leftrightarrow EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
5	1 2 4	3imtr4i	$$⊢ElDisjA\to EqvRel\sim A$$