Metamath Proof Explorer

Theorem ovexi

Description: The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis ovexi.1 
|- A = ( B F C )
Assertion ovexi 
|- A e. _V

Proof

Step Hyp Ref Expression
1 ovexi.1 
 |-  A = ( B F C )
2 ovex 
 |-  ( B F C ) e. _V
3 1 2 eqeltri 
 |-  A e. _V