Metamath Proof Explorer


Theorem cnvepima

Description: The image of converse epsilon. (Contributed by Peter Mazsa, 22-Mar-2023)

Ref Expression
Assertion cnvepima A V E -1 A = A

Proof

Step Hyp Ref Expression
1 cnvepresex A V E -1 A V
2 uniqsALTV E -1 A V A / E -1 = E -1 A
3 1 2 syl A V A / E -1 = E -1 A
4 qsid A / E -1 = A
5 4 unieqi A / E -1 = A
6 3 5 eqtr3di A V E -1 A = A