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