This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erimeq

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

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

Proof

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