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

Metamath Proof Explorer

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 A → CoElEqvRel 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-coeleqvrel ⊢ CoElEqvRel A ↔ EqvRel ≀ E -1 ↾ A
4 1 2 3 3imtr4i ⊢ ElDisj A → CoElEqvRel A