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

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