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 ) |
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 ) |