Theorem eldisjim

Description: If the elements of A are disjoint, then it has equivalent coelements (former prter1 ). Special case of disjim . (Contributed by Rodolfo Medina, 13-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 8-Feb-2018) ( Revised by Peter Mazsa, 23-Sep-2021.)

	Ref	Expression
Assertion	eldisjim	$$⊢ElDisjA\to CoElEqvRelA$$

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-coeleqvrel	$$⊢CoElEqvRelA\leftrightarrow EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
4	1 2 3	3imtr4i	$$⊢ElDisjA\to CoElEqvRelA$$