Metamath Proof Explorer

Theorem eccnvepex

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

Ref Expression
Assertion eccnvepex 
|- [ A ] `' _E e. _V

Proof

Step Hyp Ref Expression
1 snex 
 |-  { A } e. _V
2 cnvepresex 
 |-  ( { A } e. _V -> ( `' _E |` { A } ) e. _V )
3 ecexALTV 
 |-  ( ( `' _E |` { A } ) e. _V -> [ A ] `' _E e. _V )
4 1 2 3 mp2b 
 |-  [ A ] `' _E e. _V