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 ⊢ F ∈ V
Assertion fvclex ⊢ y | ∃ x y = F ⁡ x ∈ V

Proof

Step Hyp Ref Expression
1 fvclex.1 ⊢ F ∈ V
2 1 rnex ⊢ ran ⁡ F ∈ V
3 snex ⊢ ∅ ∈ V
4 2 3 unex ⊢ ran ⁡ F ∪ ∅ ∈ V
5 fvclss ⊢ y | ∃ x y = F ⁡ x ⊆ ran ⁡ F ∪ ∅
6 4 5 ssexi ⊢ y | ∃ x y = F ⁡ x ∈ V