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

Theorem brerser 38659
Description: Binary equivalence relation with natural domain and the equivalence relation with natural domain predicate are the same when 𝐴 and 𝑅 are sets. (Contributed by Peter Mazsa, 25-Aug-2021.)
Assertion
Ref Expression
brerser ((𝐴𝑉𝑅𝑊) → (𝑅 Ers 𝐴𝑅 ErALTV 𝐴))

Proof of Theorem brerser
StepHypRef Expression
1 brers 38649 . . 3 (𝐴𝑉 → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴)))
21adantr 480 . 2 ((𝐴𝑉𝑅𝑊) → (𝑅 Ers 𝐴 ↔ (𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴)))
3 eleqvrelsrel 38576 . . . . 5 (𝑅𝑊 → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅))
43adantl 481 . . . 4 ((𝐴𝑉𝑅𝑊) → (𝑅 ∈ EqvRels ↔ EqvRel 𝑅))
5 brdmqssqs 38629 . . . 4 ((𝐴𝑉𝑅𝑊) → (𝑅 DomainQss 𝐴𝑅 DomainQs 𝐴))
64, 5anbi12d 632 . . 3 ((𝐴𝑉𝑅𝑊) → ((𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴) ↔ ( EqvRel 𝑅𝑅 DomainQs 𝐴)))
7 df-erALTV 38646 . . 3 (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅𝑅 DomainQs 𝐴))
86, 7bitr4di 289 . 2 ((𝐴𝑉𝑅𝑊) → ((𝑅 ∈ EqvRels ∧ 𝑅 DomainQss 𝐴) ↔ 𝑅 ErALTV 𝐴))
92, 8bitrd 279 1 ((𝐴𝑉𝑅𝑊) → (𝑅 Ers 𝐴𝑅 ErALTV 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2106   class class class wbr 5148   EqvRels ceqvrels 38178   EqvRel weqvrel 38179   DomainQss cdmqss 38185   DomainQs wdmqs 38186   Ers cers 38187   ErALTV werALTV 38188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-ec 8746  df-qs 8750  df-rels 38467  df-ssr 38480  df-refs 38492  df-refrels 38493  df-refrel 38494  df-syms 38524  df-symrels 38525  df-symrel 38526  df-trs 38554  df-trrels 38555  df-trrel 38556  df-eqvrels 38566  df-eqvrel 38567  df-dmqss 38620  df-dmqs 38621  df-ers 38645  df-erALTV 38646
This theorem is referenced by:  mpets2  38823  pets  38834
  Copyright terms: Public domain W3C validator