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	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		cossex	⊢ ( 𝑅 ∈ 𝑉 → ≀ 𝑅 ∈ V )
2		partim	⊢ ( 𝑅 Part 𝐴 → ≀ 𝑅 ErALTV 𝐴 )
3		erimeq	⊢ ( ≀ 𝑅 ∈ V → ( ≀ 𝑅 ErALTV 𝐴 → ∼ 𝐴 = ≀ 𝑅 ) )
4	1 2 3	syl2im	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 Part 𝐴 → ∼ 𝐴 = ≀ 𝑅 ) )