Description: The result of an operation is a set. (Contributed by NM, 13Mar1995)
Ref  Expression  

Assertion  ovex   ( A F B ) e. _V 
Step  Hyp  Ref  Expression 

1  dfov   ( A F B ) = ( F ` <. A , B >. ) 

2  1  fvexi   ( A F B ) e. _V 