Theorem partimeq

Description: Partition implies that the class of coelements on the natural domain is equal to the class of cosets of the relation, cf. erimeq . (Contributed by Peter Mazsa, 25-Dec-2024)

	Ref	Expression
Assertion	partimeq	|- ( R e. V -> ( R Part A -> ~ A = ,~ R ) )

Proof

Step	Hyp	Ref	Expression
1		cossex	|- ( R e. V -> ,~ R e. _V )
2		partim	|- ( R Part A -> ,~ R ErALTV A )
3		erimeq	|- ( ,~ R e. _V -> ( ,~ R ErALTV A -> ~ A = ,~ R ) )
4	1 2 3	syl2im	|- ( R e. V -> ( R Part A -> ~ A = ,~ R ) )