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	|- ( _I Part A <-> ,~ _I ErALTV A )

Proof

Step	Hyp	Ref	Expression
1		petid2	|- ( ( Disj _I /\ ( dom _I /. _I ) = A ) <-> ( EqvRel ,~ _I /\ ( dom ,~ _I /. ,~ _I ) = A ) )
2		dfpart2	|- ( _I Part A <-> ( Disj _I /\ ( dom _I /. _I ) = A ) )
3		dferALTV2	|- ( ,~ _I ErALTV A <-> ( EqvRel ,~ _I /\ ( dom ,~ _I /. ,~ _I ) = A ) )
4	1 2 3	3bitr4i	|- ( _I Part A <-> ,~ _I ErALTV A )