As Carl remarks in comments, your formulation in the question is perfectly all right. However, if you have a good reason to want to write it down symbolically (and "because that is more mathematical" is not a good reason; it is false), then you can just do it part for part:
For every pair of elements $i$ and $j$ from $A$ ($\forall i,j\in A$) where $i$ is not equal to $j$ ($i\ne j$) it holds that ($\Rightarrow)$ the second element of the pair $i$ ($\pi_2(i)$) does not equal ($\ne$) the second element of pair $j$ ($\pi_2(j)$): $ \forall i,j\in A: i\ne j\Rightarrow \pi_2(i)\ne \pi_2(j)$ where $\pi_2$ is the second projection function. If you don't want to use the $\pi_2$, you can write $ \forall \langle a,b\rangle, \langle c,d\rangle\in A: \langle a,b\rangle\ne\langle c,d\rangle\Rightarrow b\ne d$ or a bit shorter as $ \forall \langle a,b\rangle, \langle c,d\rangle\in A: b=d\Rightarrow a=c$ If you're in a completely formal setting where you can't quantify over patterns such as $\langle a,b\rangle$, you'll need to do something like $ \forall a,b,x: \langle a,x\rangle\in A\land \langle b,x\rangle\in A\Rightarrow a=b$
Since quantifiers are involved here, the logic is (first-order) predicate calculus.
By the way, the usual name for a 2-tuple, except (possibly) when you're speaking to machines instead of to people, is an ordered pair.