Metamath Proof Explorer


Theorem cnvepimaex

Description: The image of converse epsilon exists, proof via imaexALTV (see also cnvepima and uniexg for alternate way). (Contributed by Peter Mazsa, 22-Mar-2023)

Ref Expression
Assertion cnvepimaex
|- ( A e. V -> ( `' _E " A ) e. _V )

Proof

Step Hyp Ref Expression
1 cnvepresex
 |-  ( A e. V -> ( `' _E |` A ) e. _V )
2 imaexALTV
 |-  ( ( `' _E e. _V \/ ( ( `' _E |` A ) e. _V /\ A e. V ) ) -> ( `' _E " A ) e. _V )
3 2 olcs
 |-  ( ( ( `' _E |` A ) e. _V /\ A e. V ) -> ( `' _E " A ) e. _V )
4 1 3 mpancom
 |-  ( A e. V -> ( `' _E " A ) e. _V )