Theorem dferALTV2

Description: Equivalence relation with natural domain predicate, see the comment of df-ers . (Contributed by Peter Mazsa, 26-Jun-2021) (Revised by Peter Mazsa, 30-Aug-2021)

	Ref	Expression
Assertion	dferALTV2	$$⊢RErALTVA\leftrightarrow \left(EqvRelR\wedge \mathrm{dom}R/R=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-erALTV	$$⊢RErALTVA\leftrightarrow \left(EqvRelR\wedge RDomainQsA\right)$$
2		df-dmqs	$$⊢RDomainQsA\leftrightarrow \mathrm{dom}R/R=A$$
3	2	anbi2i	$$⊢\left(EqvRelR\wedge RDomainQsA\right)\leftrightarrow \left(EqvRelR\wedge \mathrm{dom}R/R=A\right)$$
4	1 3	bitri	$$⊢RErALTVA\leftrightarrow \left(EqvRelR\wedge \mathrm{dom}R/R=A\right)$$