This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnvepima

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

Ref Expression
Assertion cnvepima ⊢ A ∈ V → E -1 A = ⋃ A

Proof

Step Hyp Ref Expression
1 cnvepresex ⊢ A ∈ V → E -1 ↾ A ∈ V
2 uniqs ⊢ E -1 ↾ A ∈ V → ⋃ A / E -1 = E -1 A
3 1 2 syl ⊢ A ∈ V → ⋃ A / E -1 = E -1 A
4 qsid ⊢ A / E -1 = A
5 4 unieqi ⊢ ⋃ A / E -1 = ⋃ A
6 3 5 eqtr3di ⊢ A ∈ V → E -1 A = ⋃ A