Metamath Proof Explorer


Theorem eccnvep

Description: The converse epsilon coset of a set is the set. (Contributed by Peter Mazsa, 27-Jan-2019)

Ref Expression
Assertion eccnvep ( 𝐴𝑉 → [ 𝐴 ] E = 𝐴 )

Proof

Step Hyp Ref Expression
1 eleccnvep ( 𝐴𝑉 → ( 𝑥 ∈ [ 𝐴 ] E ↔ 𝑥𝐴 ) )
2 1 eqrdv ( 𝐴𝑉 → [ 𝐴 ] E = 𝐴 )