Theorem erim

Description: Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most convenient form of prter3 and erim2 ). (Contributed by Peter Mazsa, 7-Oct-2021) (Revised by Peter Mazsa, 29-Dec-2021)

	Ref	Expression
Assertion	erim	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		dferALTV2	⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) )
2		erim2	⊢ ( 𝑅 ∈ 𝑉 → ( ( EqvRel 𝑅 ∧ ( dom 𝑅 / 𝑅 ) = 𝐴 ) → ∼ 𝐴 = 𝑅 ) )
3	1 2	syl5bi	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅 ) )