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

Metamath Proof Explorer

Theorem petid

Description: A class is a partition by the identity class if and only if the cosets by the identity class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021)

Ref Expression
Assertion petid ⊢ I Part A ↔ ≀ I ErALTV A

Proof

Step Hyp Ref Expression
1 petid2 ⊢ Disj I ∧ dom ⁡ I / I = A ↔ EqvRel ≀ I ∧ dom ⁡ ≀ I / ≀ I = A
2 dfpart2 ⊢ I Part A ↔ Disj I ∧ dom ⁡ I / I = A
3 dferALTV2 ⊢ ≀ I ErALTV A ↔ EqvRel ≀ I ∧ dom ⁡ ≀ I / ≀ I = A
4 1 2 3 3bitr4i ⊢ I Part A ↔ ≀ I ErALTV A