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 AVAE-1=A

Proof

Step Hyp Ref Expression
1 eleccnvep AVxAE-1xA
2 1 eqrdv AVAE-1=A