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	⊢ ( ElDisj 𝐴 → CoElEqvRel 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		disjim	⊢ ( Disj ( ◡ E ↾ 𝐴 ) → EqvRel ≀ ( ◡ E ↾ 𝐴 ) )
2		df-eldisj	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
3		df-coeleqvrel	⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )
4	1 2 3	3imtr4i	⊢ ( ElDisj 𝐴 → CoElEqvRel 𝐴 )