Metamath Proof Explorer

Theorem fvex

Description: The value of a class exists. Corollary 6.13 of TakeutiZaring p. 27. (Contributed by NM, 30-Dec-1996)

Ref Expression
Assertion fvex 
|- ( F ` A ) e. _V

Proof

Step Hyp Ref Expression
1 df-fv 
 |-  ( F ` A ) = ( iota x A F x )
2 iotaex 
 |-  ( iota x A F x ) e. _V
3 1 2 eqeltri 
 |-  ( F ` A ) e. _V