What do the ∀ and ∃ symbols mean in the Axiom of Choice?

Question

On the Wikipedia page for the Axiom of Choice the following statement is given:

$(\forall x^\sigma)(\exists y^\tau)R(x,y)\rightarrow(\exists f^{\sigma \rightarrow \tau})(\forall x^\sigma)R(x, f(x))$

Most of it seems fairly straightforward, except for the meanings of the symbols that look like 180 degree rotated 'E' and 'A'

Answer 1

The symbols are quantifiers. They bind a new variable name to the symbolic logic statements. ∃ reads as there exists. ∀ reads for all so the first part of the statement would be read as:

forall x (of type 𝜎), there exists a y (of type 𝜏) such that ...

Answer 2

$\forall$ reads as "for all", and $\exists$ reads as "there exists". So, in english we have

$$\text{"if }\underbrace{\text{for all $x$}}_{\forall x^\sigma}\text{ }\underbrace{\text{exists a $y$}}_{\exists y^\tau}\text{ with $R(x,y)$, }\underbrace{\text{then}}_\to\text{ }\underbrace{\text{there is a function $f$}}_{\exists f^{\sigma\to\tau}}\text{ so that }\underbrace{\text{for all $x$}}_{\forall x^\sigma}\text{ holds $R(x,f(x))$".}$$

I skipped over the $\sigma$ and $\tau$ superscripts, as they indicate types and are not of primary importance here.