Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-erALTV Structured version   Visualization version   GIF version

Definition df-erALTV 36755
Description: Equivalence relation with natural domain predicate, see also the comment of df-ers 36754. Alternate definition is dferALTV2 36759. Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets, see brerser 36767. (Contributed by Peter Mazsa, 12-Aug-2021.)
Assertion
Ref Expression
df-erALTV (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅𝑅 DomainQs 𝐴))

Detailed syntax breakdown of Definition df-erALTV
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2werALTV 36338 . 2 wff 𝑅 ErALTV 𝐴
42weqvrel 36329 . . 3 wff EqvRel 𝑅
51, 2wdmqs 36336 . . 3 wff 𝑅 DomainQs 𝐴
64, 5wa 395 . 2 wff ( EqvRel 𝑅𝑅 DomainQs 𝐴)
73, 6wb 205 1 wff (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅𝑅 DomainQs 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  dferALTV2  36759  brerser  36767
  Copyright terms: Public domain W3C validator