Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Functions
imaexi
Next ⟩
axccdom
Metamath Proof Explorer
Ascii
Unicode
Theorem
imaexi
Description:
The image of a set is a set.
(Contributed by
Glauco Siliprandi
, 26-Jun-2021)
Ref
Expression
Hypothesis
imaexi.1
⊢
A
∈
V
Assertion
imaexi
⊢
A
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
imaexi.1
⊢
A
∈
V
2
imaexg
⊢
A
∈
V
→
A
B
∈
V
3
1
2
ax-mp
⊢
A
B
∈
V