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

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 ⊢ 𝐹 ∈ V
Assertion fvclex { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) } ∈ V

Proof

Step Hyp Ref Expression
1 fvclex.1 ⊢ 𝐹 ∈ V
2 1 rnex ⊢ ran 𝐹 ∈ V
3 snex ⊢ { ∅ } ∈ V
4 2 3 unex ⊢ ( ran 𝐹 ∪ { ∅ } ) ∈ V
5 fvclss ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) } ⊆ ( ran 𝐹 ∪ { ∅ } )
6 4 5 ssexi ⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = ( 𝐹 ‘ 𝑥 ) } ∈ V