**Description:** The result of an operation is a set. (Contributed by NM, 13-Mar-1995)

Ref | Expression | ||
---|---|---|---|

Assertion | ovex | $${\u22a2}{A}{F}{B}\in \mathrm{V}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | df-ov | $${\u22a2}{A}{F}{B}={F}\left(\u27e8{A},{B}\u27e9\right)$$ | |

2 | 1 | fvexi | $${\u22a2}{A}{F}{B}\in \mathrm{V}$$ |