Metamath Proof Explorer

Theorem petidres2

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

Ref Expression
Assertion petidres2 ⊢ Disj I ↾ A ∧ dom ⁡ I ↾ A / I ↾ A = A ↔ EqvRel ≀ I ↾ A ∧ dom ⁡ ≀ I ↾ A / ≀ I ↾ A = A

Proof

Step Hyp Ref Expression
1 disjALTVidres ⊢ Disj I ↾ A
2 1 petlemi ⊢ Disj I ↾ A ∧ dom ⁡ I ↾ A / I ↾ A = A ↔ EqvRel ≀ I ↾ A ∧ dom ⁡ ≀ I ↾ A / ≀ I ↾ A = A