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