Metamath Proof Explorer

Theorem petidres

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

Ref Expression
Assertion petidres ⊢ I ↾ A Part A ↔ ≀ I ↾ A ErALTV A

Proof

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