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

Theorem erim 36353
 Description: Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is the most convenient form of prter3 36459 and erim2 36352). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.)
Assertion
Ref Expression
erim (𝑅𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))

Proof of Theorem erim
StepHypRef Expression
1 dferALTV2 36343 . 2 (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
2 erim2 36352 . 2 (𝑅𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅))
31, 2syl5bi 245 1 (𝑅𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539   ∈ wcel 2112  dom cdm 5525   / cqs 8299   ∼ ccoels 35895   EqvRel weqvrel 35911   ErALTV werALTV 35920 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299  ax-un 7460 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-id 5431  df-eprel 5436  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-ec 8302  df-qs 8306  df-coss 36100  df-coels 36101  df-refrel 36193  df-symrel 36221  df-trrel 36251  df-eqvrel 36261  df-dmqs 36315  df-erALTV 36339 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator