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	$$⊢\mathrm{I}PartA\leftrightarrow \wr \mathrm{I}ErALTVA$$

Proof

Step	Hyp	Ref	Expression
1		petid2	$$⊢\left(Disj\mathrm{I}\wedge \mathrm{dom}\mathrm{I}/\mathrm{I}=A\right)\leftrightarrow \left(EqvRel\wr \mathrm{I}\wedge \mathrm{dom}\wr \mathrm{I}/\wr \mathrm{I}=A\right)$$
2		dfpart2	$$⊢\mathrm{I}PartA\leftrightarrow \left(Disj\mathrm{I}\wedge \mathrm{dom}\mathrm{I}/\mathrm{I}=A\right)$$
3		dferALTV2	$$⊢\wr \mathrm{I}ErALTVA\leftrightarrow \left(EqvRel\wr \mathrm{I}\wedge \mathrm{dom}\wr \mathrm{I}/\wr \mathrm{I}=A\right)$$
4	1 2 3	3bitr4i	$$⊢\mathrm{I}PartA\leftrightarrow \wr \mathrm{I}ErALTVA$$