Metamath Proof Explorer

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 ∈ V ∧ R ∈ W → R Ers A ↔ R ErALTV A

Proof

Step Hyp Ref Expression
1 brers ⊢ A ∈ V → R Ers A ↔ R ∈ EqvRels ∧ R DomainQss A
2 1 adantr ⊢ A ∈ V ∧ R ∈ W → R Ers A ↔ R ∈ EqvRels ∧ R DomainQss A
3 eleqvrelsrel ⊢ R ∈ W → R ∈ EqvRels ↔ EqvRel R
4 3 adantl ⊢ A ∈ V ∧ R ∈ W → R ∈ EqvRels ↔ EqvRel R
5 brdmqssqs ⊢ A ∈ V ∧ R ∈ W → R DomainQss A ↔ R DomainQs A
6 4 5 anbi12d ⊢ A ∈ V ∧ R ∈ W → R ∈ 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 ∈ V ∧ R ∈ W → R ∈ EqvRels ∧ R DomainQss A ↔ R ErALTV A
9 2 8 bitrd ⊢ A ∈ V ∧ R ∈ W → R Ers A ↔ R ErALTV A