Description: Class A is a partition by the null class if and only if the cosets by the null class are in equivalence relation on it. (Contributed by Peter Mazsa, 31-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pet02 | |- ( ( Disj (/) /\ ( dom (/) /. (/) ) = A ) <-> ( EqvRel ,~ (/) /\ ( dom ,~ (/) /. ,~ (/) ) = A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | disjALTV0 | |- Disj (/) |
|
| 2 | 1 | petlemi | |- ( ( Disj (/) /\ ( dom (/) /. (/) ) = A ) <-> ( EqvRel ,~ (/) /\ ( dom ,~ (/) /. ,~ (/) ) = A ) ) |