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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Ers 𝐴 ↔ ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ers	⊢ Ers = ( DomainQss ↾ EqvRels )
2	1	eqres	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Ers 𝐴 ↔ ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ) )