Theorem erimeq

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 erimeq2 ). (Contributed by Peter Mazsa, 7-Oct-2021) (Revised by Peter Mazsa, 29-Dec-2021)

	Ref	Expression
Assertion	erimeq	$$⊢R\in V\to \left(RErALTVA\to \sim A=R\right)$$

Proof

Step	Hyp	Ref	Expression
1		dferALTV2	$$⊢RErALTVA\leftrightarrow \left(EqvRelR\wedge \mathrm{dom}R/R=A\right)$$
2		erimeq2	$$⊢R\in V\to \left(\left(EqvRelR\wedge \mathrm{dom}R/R=A\right)\to \sim A=R\right)$$
3	1 2	biimtrid	$$⊢R\in V\to \left(RErALTVA\to \sim A=R\right)$$