Description: The converse epsilon coset exists. (Contributed by Peter Mazsa, 22-Mar-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eccnvepex | ⊢ [ 𝐴 ] ◡ E ∈ V |
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 |