Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
ovex
Next ⟩
ovexi
Metamath Proof Explorer
Ascii
Unicode
Theorem
ovex
Description:
The result of an operation is a set.
(Contributed by
NM
, 13-Mar-1995)
Ref
Expression
Assertion
ovex
⊢
A
F
B
∈
V
Proof
Step
Hyp
Ref
Expression
1
df-ov
⊢
A
F
B
=
F
⁡
A
B
2
1
fvexi
⊢
A
F
B
∈
V