Description: Class A 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 | petid2 | |- ( ( Disj _I /\ ( dom _I /. _I ) = A ) <-> ( EqvRel ,~ _I /\ ( dom ,~ _I /. ,~ _I ) = A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | disjALTVid | |- Disj _I |
|
| 2 | 1 | petlemi | |- ( ( Disj _I /\ ( dom _I /. _I ) = A ) <-> ( EqvRel ,~ _I /\ ( dom ,~ _I /. ,~ _I ) = A ) ) |