Metamath Proof Explorer

Theorem fvexi

Description: The value of a class exists. Inference form of fvex . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 fvexi.1 
 |-  A = ( F ` B )
2 fvex 
 |-  ( F ` B ) e. _V
3 1 2 eqeltri 
 |-  A e. _V