Theorem petidres2

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

	Ref	Expression
Assertion	petidres2	|- ( ( Disj ( _I |` A ) /\ ( dom ( _I |` A ) /. ( _I |` A ) ) = A ) <-> ( EqvRel ,~ ( _I |` A ) /\ ( dom ,~ ( _I |` A ) /. ,~ ( _I |` A ) ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		disjALTVidres	|- Disj ( _I |` A )
2	1	petlemi	|- ( ( Disj ( _I |` A ) /\ ( dom ( _I |` A ) /. ( _I |` A ) ) = A ) <-> ( EqvRel ,~ ( _I |` A ) /\ ( dom ,~ ( _I |` A ) /. ,~ ( _I |` A ) ) = A ) )