Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Peter Mazsa
Preparatory theorems
cnvepima
Next ⟩
inex3
Metamath Proof Explorer
Ascii
Unicode
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
uniqsALTV
⊢
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