Metamath Proof Explorer

Theorem fvclex

Description: Existence of the class of values of a set. (Contributed by NM, 9-Nov-1995)

Ref Expression
Hypothesis fvclex.1 
|- F e. _V
Assertion fvclex 
|- { y | E. x y = ( F ` x ) } e. _V

Proof

Step Hyp Ref Expression
1 fvclex.1 
 |-  F e. _V
2 1 rnex 
 |-  ran F e. _V
3 snex 
 |-  { (/) } e. _V
4 2 3 unex 
 |-  ( ran F u. { (/) } ) e. _V
5 fvclss 
 |-  { y | E. x y = ( F ` x ) } C_ ( ran F u. { (/) } )
6 4 5 ssexi 
 |-  { y | E. x y = ( F ` x ) } e. _V