This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) e. _V

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A F B ) = ( F ` <. A , B >. )
2 1 fvexi 
 |-  ( A F B ) e. _V