Theorem erimeq 39441

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 39684 and erimeq2 39440). (Contributed by Peter Mazsa, 7-Oct-2021.) (Revised by Peter Mazsa, 29-Dec-2021.)

Assertion

Ref	Expression
erimeq	⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))

Proof of Theorem erimeq

Step	Hyp	Ref	Expression
1		dferALTV2 39430	. 2 ⊢ (𝑅 ErALTV 𝐴 ↔ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴))
2		erimeq2 39440	. 2 ⊢ (𝑅 ∈ 𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅))
3	1, 2	biimtrid 245	1 ⊢ (𝑅 ∈ 𝑉 → (𝑅 ErALTV 𝐴 → ∼ 𝐴 = 𝑅))

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  dom cdm 5661   / cqs 8689   ∼ ccoels 38861   EqvRel weqvrel 38877   ErALTV werALTV 38886

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-11 2192  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-id 5556  df-eprel 5561  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ec 8692  df-qs 8696  df-coss 39178  df-coels 39179  df-refrel 39269  df-symrel 39301  df-trrel 39335  df-eqvrel 39346  df-dmqs 39400  df-erALTV 39426

This theorem is used by:  partimeq  39589