Theorem petidres

Description: A class is a partition by identity class restricted to it if and only if the cosets by the restricted identity class are in equivalence relation on it, cf. eqvrel1cossidres . (Contributed by Peter Mazsa, 31-Dec-2021)

	Ref	Expression
Assertion	petidres	|- ( ( _I |` A ) Part A <-> ,~ ( _I |` A ) ErALTV A )

Proof

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