Rotating a vector perpendicular to another?

Suppose I have two unit vectors $$(x_1,x_2,x_3)$$ and $$(y_1,y_2,y_3)$$ in 3D space that are perpendicular to each other. (Their dot product is zero.)

I want to rotate the $$x$$ vector by $$\theta$$ degrees such that it remains perpendicular to $$y$$. That is, I want to rotate $$x$$ using $$y$$ as the axis.

What would be the formula to do this and how is it derived?

I will give you a general formula, where $$\vec x$$ and $$\vec y$$ are not necessarily unit vectors.

Assume $$\Vert\vec x\Vert, \Vert\vec y\Vert \not= 0$$ and they are not collinear. Call the resulting (rotated) vector $$\vec x'$$. First, let's get a vector that is perpendicular to $$\vec y$$. One such vector is $$\vec x\times \vec y$$, but for convenience, we will consider the vector $$\vec z = \frac{\vec x\times \vec y}{\Vert\vec y\Vert}$$. Note that $$\Vert \vec z \Vert=\Vert \vec x \Vert$$.

This vector is perpendicular to $$\vec x$$ as well. Because $$\vec x'$$ lies in the same plane as $$\vec x$$ and $$\vec z$$, it can be expressed as their linear combination, i.e.

$$\vec x' = \alpha \vec x + \beta \vec z$$ Multiplying (dot product) both sides with $$\vec x$$, we get

$$\vec x \cdot \vec x' = \alpha \vec x^2 + \beta \vec z \cdot \vec x = \alpha \vec x^2 \tag1$$ We used the fact that $$\vec z$$ is perpendicular to $$\vec x$$, making their dot product zero. Because $$\Vert \vec x' \Vert = \Vert \vec x \Vert$$, we have that $$\vec x \cdot \vec x' = \Vert \vec x \Vert^2\cos\theta$$. This, combined with $$(1)$$ gives us $$\alpha = \cos\theta$$. Using the fact that $$\Vert \vec z \Vert = \Vert \vec x \Vert$$ it can easily be shown that $$\beta=\sin\theta$$.

So, your vector is $$\vec x' = \cos\theta\cdot \vec x + \sin\theta\cdot \vec z$$

Notice that I haven't mentioned in which direction the vector is rotated. I will leave this for you to figure out.