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	Could not format assertion : No typesetting found for |- ( _I Part A <-> ,~ _I ErALTV A ) with typecode |-

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	Could not format ( _I Part A <-> ( Disj _I /\ ( dom _I /. _I ) = A ) ) : No typesetting found for |- ( _I Part A <-> ( Disj _I /\ ( dom _I /. _I ) = A ) ) with typecode |-
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	Could not format ( _I Part A <-> ,~ _I ErALTV A ) : No typesetting found for |- ( _I Part A <-> ,~ _I ErALTV A ) with typecode |-