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

Proof

Step	Hyp	Ref	Expression
1		brers	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑅 Ers 𝐴 ↔ ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 Ers 𝐴 ↔ ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ) )
3		eleqvrelsrel	⊢ ( 𝑅 ∈ 𝑊 → ( 𝑅 ∈ EqvRels ↔ EqvRel 𝑅 ) )
4	3	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 ∈ EqvRels ↔ EqvRel 𝑅 ) )
5		brdmqssqs	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 DomainQss 𝐴 ↔ 𝑅 DomainQs 𝐴 ) )
6	4 5	anbi12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 ) ) )
7		df-erALTV	⊢ ( 𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴 ) )
8	6 7	bitr4di	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ( 𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴 ) ↔ 𝑅 ErALTV 𝐴 ) )
9	2 8	bitrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 Ers 𝐴 ↔ 𝑅 ErALTV 𝐴 ) )