Metamath Proof Explorer

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 e. V -> ( R Ers A <-> ( R e. EqvRels /\ R DomainQss A ) ) )

Proof

Step Hyp Ref Expression
1 df-ers 
 |-  Ers = ( DomainQss |` EqvRels )
2 1 eqres 
 |-  ( A e. V -> ( R Ers A <-> ( R e. EqvRels /\ R DomainQss A ) ) )