Theorem brerser

Description: Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when A and R are sets. (Contributed by Peter Mazsa, 25-Aug-2021)

	Ref	Expression
Assertion	brerser	|- ( ( A e. V /\ R e. W ) -> ( R Ers A <-> R ErALTV A ) )

Proof

Step	Hyp	Ref	Expression
1		brers	|- ( A e. V -> ( R Ers A <-> ( R e. EqvRels /\ R DomainQss A ) ) )
2	1	adantr	|- ( ( A e. V /\ R e. W ) -> ( R Ers A <-> ( R e. EqvRels /\ R DomainQss A ) ) )
3		eleqvrelsrel	|- ( R e. W -> ( R e. EqvRels <-> EqvRel R ) )
4	3	adantl	|- ( ( A e. V /\ R e. W ) -> ( R e. EqvRels <-> EqvRel R ) )
5		brdmqssqs	|- ( ( A e. V /\ R e. W ) -> ( R DomainQss A <-> R DomainQs A ) )
6	4 5	anbi12d	|- ( ( A e. V /\ R e. W ) -> ( ( R e. EqvRels /\ R DomainQss A ) <-> ( EqvRel R /\ R DomainQs A ) ) )
7		df-erALTV	|- ( R ErALTV A <-> ( EqvRel R /\ R DomainQs A ) )
8	6 7	bitr4di	|- ( ( A e. V /\ R e. W ) -> ( ( R e. EqvRels /\ R DomainQss A ) <-> R ErALTV A ) )
9	2 8	bitrd	|- ( ( A e. V /\ R e. W ) -> ( R Ers A <-> R ErALTV A ) )