Theorem petid2

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	$$⊢\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)$$

Proof

Step	Hyp	Ref	Expression
1		disjALTVid	$$⊢Disj\mathrm{I}$$
2	1	petlemi	$$⊢\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)$$