Definition df-erALTV 36776

Description: Equivalence relation with natural domain predicate, see also the comment of df-ers 36775. Alternate definition is dferALTV2 36780. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 36788. (Contributed by Peter Mazsa, 12-Aug-2021.)

Assertion

Ref	Expression
df-erALTV	⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴))

Detailed syntax breakdown of Definition df-erALTV

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	werALTV 36359	. 2 wff 𝑅 ErALTV 𝐴
4	2	weqvrel 36350	. . 3 wff EqvRel 𝑅
5	1, 2	wdmqs 36357	. . 3 wff 𝑅 DomainQs 𝐴
6	4, 5	wa 396	. 2 wff ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴)
7	3, 6	wb 205	1 wff (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ 𝑅 DomainQs 𝐴))

This definition is referenced by:  dferALTV2  36780  brerser  36788