Metamath Proof Explorer


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