Metamath Proof Explorer


Theorem eccnvepex

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

Ref Expression
Assertion eccnvepex [ 𝐴 ] E ∈ V

Proof

Step Hyp Ref Expression
1 snex { 𝐴 } ∈ V
2 cnvepresex ( { 𝐴 } ∈ V → ( E ↾ { 𝐴 } ) ∈ V )
3 ecexALTV ( ( E ↾ { 𝐴 } ) ∈ V → [ 𝐴 ] E ∈ V )
4 1 2 3 mp2b [ 𝐴 ] E ∈ V