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
qsid
⊢
A
/
E
-1
=
A
2
1
unieqi
⊢
⋃
A
/
E
-1
=
⋃
A
3
cnvepresex
⊢
A
∈
V
→
E
-1
↾
A
∈
V
4
uniqsALTV
⊢
E
-1
↾
A
∈
V
→
⋃
A
/
E
-1
=
E
-1
A
5
3
4
syl
⊢
A
∈
V
→
⋃
A
/
E
-1
=
E
-1
A
6
2
5
syl5reqr
⊢
A
∈
V
→
E
-1
A
=
⋃
A