Proof of Membership in the Line ℝx₀ of a Real Vector Space

The condition "there is $t\in\mathbb{R}$ with $y=tx_{0}$" quantifies only over the set variable $t$, and $y=tx_{0}$ is an equation between $y$ and a value of the scalar multiplication; so the condition is predicative, with parameters $\mathbb{R}$, $x_{0}$ and the scalar multiplication. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (i), for every set $y$ we have $y\in\mathbb{R}x_{0}$ if and only if there is $t\in\mathbb{R}$ with $y=tx_{0}$.

Now let $y$ be a class. If $y\in\mathbb{R}x_{0}$, then $y$ is a set by Classes, Membership, Sets and Proper Classes (i), and the equivalence for sets gives $t$. Conversely, if $y=tx_{0}$ with $t\in\mathbb{R}$, then $y\in V$, because the scalar multiplication of Vector Space over a Field is a function from $\mathbb{R}\times V$ to $V$; so $y$ is a set by Classes, Membership, Sets and Proper Classes (i), and the equivalence for sets gives $y\in\mathbb{R}x_{0}$.