In Kenneth Kunen's book The Foundations of Mathematics, there is a definition of a mathematical definition : it is an conservative extension $\mathcal L'$ of a language $\mathcal L$ of a theory $T$. More precisely, to define a new $n$-ary relation $\phi$ in $T$ is to add "$\phi$" to $\mathcal L$ and add an axiom of the form : $$\forall x_1,\ldots,\forall x_n (\phi(x_1,\ldots,x_n)\Leftrightarrow R(x_1,\ldots,x_n))$$ where $R$ is a $n$-ary relation already included in the base language $\mathcal L$. So far so good.
But what about what I could call a "conditional" definition ? By that expression I mean a property that is only defined over a subset of the universe. For example, in a theory of real numbers, I could define the predicate "$n$ is even" only when $n$ is a natural number. I would proceed in this manner :
(Let's recall that we work with the real numbers.)
Definition. Let $n$ be a natural number. We say that $n$ in even if and only if $n/2$ is a natural number.
A consequence is that the number $\pi$ is not even nor non-even, it makes no sense to talk about the evenness of non-natural numbers. Mathematics are full of that kind of definitions (I think of "$f$ is continuous at $a$" where $a$ is not any number but member of the domain of $f$).
My question is :
How to formalize that kind of "conditional" definition ?
I would try this. Add a predicate symbol $E$ to the base language ("$Ex"$ would mean "$x$ is even") and the following axiom : $$\forall x(x\in\mathbb N\Rightarrow (Ex\Leftrightarrow x/2\in\mathbb N))$$ But this doesn't correspond to Kunen's definition of a mathematical definition.
So is it a good way to formalize a "conditional" definition ? In particular, is that process a conservative extension of the base theory ?