$\forall$ is "distributiv" Recently I stumbled upon an equivalence in analysis which is of the
form $\forall x\varphi(x)\leftrightarrow\forall x\psi(x)$. This made
me wonder if this is mabe equivalent to $\forall x(\varphi(x)\leftrightarrow\psi(x))$,
i.e. if "$\forall$" is "distributiv" w.r.t. $\varphi$
and $\psi$.
My questions are:


*

*Does it even make sense to ask if $\forall x\varphi(x)\leftrightarrow\forall x\psi(x)$
is equivalent to $\forall x(\varphi(x)\leftrightarrow\psi(x))$, without
specifying some " framework" within which this question has
to be answered ? (Like for example the Hilbert system or in the sense
of being true in all models ?)

*Is it the case that $\forall x\varphi(x)\leftrightarrow\forall x\psi(x)$
is indeed equivalent to $\forall x(\varphi(x)\leftrightarrow\psi(x))$
?

*For those who want to know, how I arrived at this question:*$\varphi$
is the triangle inequality 
$$
\forall x,y\in\mathbb{R}:\ \left|x+y\right|\leqslant\left|x\right|+\left|y\right|\quad\quad\quad(1),
$$
and $\psi$ the similar inequality 
$$
\forall x,y\in\mathbb{R}:\ \left|x-y\right|\leqslant\left|x\right|+\left|y\right|\quad\quad\quad(2),
$$
and I wanted to show that $(1)$ and $(2)$ are equivalent. (The proof
is short: If I know that $(1)$ is true, and want to prove $(2)$,
I take some arbitrary $x,y\in\mathbb{R}$ and plug, $x,-y$ in $(1)$
and obtain that $(2)$ -- and similarly for the other implication.)
This made me question, if 
$$
\forall x,y\in\mathbb{R}:\ \left|x+y\right|\leqslant\left|x\right|+\left|y\right|\ \longleftrightarrow\ \left|x-y\right|\leqslant\left|x\right|+\left|y\right|
$$
also were true -- but I couldn't prove it using "usual mathematics",
so I wondered this maybe is an instance of a general logical rule.
 A: Answering the first question, it doesn't make sense to formally ask anything without a formal theory. Informally it makes sense, everything does (or anything doesn't).
Answering the second question, with the standard 'meaning' for $\forall$ and $\to$ and given one-place predicates $\varphi$ and $\psi$ , it isn't true that $$\forall x\varphi(x)\leftrightarrow \forall x\psi (x)\iff \forall x(\varphi(x)\leftrightarrow \psi(x)).$$
As an example, in $\sf ZFC$, let
$$\varphi(x): x\text{ is a real number and }x>0,$$
$$\psi(x): x\text{ is a real number and }x\text{ is invertible}.$$
Clearly $\forall x(\varphi(x)\leftrightarrow \psi(x))$ is false as there are negative invertible elements and $\forall x\varphi(x)\leftrightarrow \forall x\psi (x)$ is true because both $\forall x\varphi(x)$ and  $\forall x\psi (x)$ are false.
Recall that $\leftrightarrow$ is expendable if you have $\neg$ and $\lor$. With this in mind one would suspect the equivalence couldn't possibly hold because of the non-distributivy of $\forall$ over $\lor$.
A: It doesn't make sense to ask the question without any framework, but you're certainly working in some first-order predicate logic.  It makes sense to ask whether the statements are logically equivalent.
They're not equivalent in this generality, however.  You can check this by constructing an example structure where one statement holds but the other doesn't.  If they were equivalent, they'd have to have the same truth value wherever you interpret them.
E.g.: Our structure will consist of 2 objects $\{A, B\}$, and we'll use two predicates $\phi$ and $\psi$ which we'll interpret so that
$\phi(A)$ is true
$\psi(A)$ is false
$\phi(B)$ is false
$\psi(B)$ is true
In this structure, $\forall x\phi(x)$ and $\forall x \psi(x)$ are false, so $\forall x \phi(x) \leftrightarrow \forall x \psi(x)$ is true, but $\forall x (\phi(x)\leftrightarrow \psi(x))$ is false.
As a side note, the implication does hold one way in general: if $\forall x (\phi(x)\leftrightarrow\psi(x))$, then $\forall x \phi(x) \leftrightarrow \forall x \psi(x)$.  So, you can "distribute" it across, which makes it weaker, but you can't generally "factor it out".
A: You might want to look at Skolemization in which we move the all quatifiers to the left end of the expression owing to some of its distributive properties. the Even though what you said is false in general, a list of distributive laws which actually works can be found here (2.13 (d))
A: This is a partial answer given for the sake of it. Hence why I've made it community wiki.
The following is constructed from a path of a tableau, which I could produce here if you like (but it will take a while).
Suppose $$\color{red}{(\forall x\varphi(x)\leftrightarrow \forall x\psi (x))}\leftrightarrow \color{blue}{\forall x(\varphi(x)\leftrightarrow \psi(x))}.$$ Then if $\color{red}{\neg (\forall x\varphi(x)\leftrightarrow \forall x\psi (x))}$ holds, then $\color{blue}{\neg \forall x(\varphi(x)\leftrightarrow \psi(x))}$ holds and so we can "instantiate" and say that there exists an $\color{blue}{a}$ such that $$\color{blue}{\neg (\varphi(a)\leftrightarrow \psi(a))}.$$ Assume $\color{blue}{\varphi(a)}$. Now $\color{blue}{\neg\psi(a)}$, but from $\color{red}{\neg (\forall x\varphi(x)\leftrightarrow \forall x\psi (x))}$, if we also assume $\color{red}{\neg\forall x\varphi(x)}$, we get $\color{red}{\forall x\psi(x)}$, giving $\color{red}{\psi(a)}$, a contradiction.
