Theorem brers

Description: Binary equivalence relation with natural domain, see the comment of df-ers . (Contributed by Peter Mazsa, 23-Jul-2021)

	Ref	Expression
Assertion	brers	$$⊢A\in V\to \left(R\mathrm{Ers}A\leftrightarrow \left(R\in \mathrm{EqvRels}\wedge R\mathrm{DomainQss}A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ers	$$⊢\mathrm{Ers}={\mathrm{DomainQss}\upharpoonright }_{\mathrm{EqvRels}}$$
2	1	eqres	$$⊢A\in V\to \left(R\mathrm{Ers}A\leftrightarrow \left(R\in \mathrm{EqvRels}\wedge R\mathrm{DomainQss}A\right)\right)$$