What character can replace word "let" in proofs? For example, suppose I have a line of a proof introducing new “variable” $x$:
$$\textrm{Let}\:\:x\in f(y)$$
I am looking for ways to express the word “let” in this context and I would like to avoid using natural language because Math is itself a universal language for expressing complex ideas.
I used to use a character like a right square bracket or similar to it. I once encountered it somewhere, but I don't know if it is a common practice. For example, I would write that line like this:
$$\sqsupset x\in f(y)$$
Now I failed to find this character anywhere, neither on the Web nor in Unicode symbol set. Instead, I discovered some similar symbols like $\buildrel \text{def}\over=$, or $:=$, or $\buildrel\triangle\over=$, or $:\Leftrightarrow$ in Wikipedia, but those are very limited and not so much useful in my case.
 A: 
I would like to avoid using natural language because Math is itself a universal language for expressing complex ideas.

Honestly, I think this is a bad (by which I mean non-mathematical) reason to do anything. You will have great difficulty introducing any symbol into any widespread use, and consequently you will not be able to use such a symbol in any piece of work you wish to be taken seriously (because nobody will be able to read it!). I also don't recommend you teach people bad habits.
On the other hand, if these are just for personal notes, by all means invent your own symbol. I use lots of imprecise squiggly arrows, equals signs with quotation marks round them, equals signs decorated with question marks, and the like. I often use := to conjure a symbol into existence at the same time as defining it (because, unlike when programming, I don't need to declare my variables and I don't often redefine them in the same 'subroutine'), or simply =. I've seen people write an equals sign with "def" or "$\triangle$" above it too.
This is not unlike how real mathematicians work with each other. When two people collaborate, it's very convenient for there to be an implicit assumption along the lines of "every time I say X, until we solve this problem, I mean this particular object", or vague terminology like "nice" to describe classes of objects that you can't quite pin down. But of course, once it comes to a seminar or a paper, you start from scratch, (mostly) give everything real, sensible words, and don't force your audience to learn a page of jargon and squiggles when there's perfectly good English available for it.
A: If you're seeking to completely eliminate natural language from your proof, then it seems to me that this is synonymous with seeking to write a formal proof.  So, let me assume that, in natural language, the statement you're trying to prove is something of the form, "Let $x$ satisfy the property $\mathbf\Phi(x)$. Then $\mathbf\Psi(x)$.". Here $\mathbf\Phi(x)$ and $\mathbf\Psi(x)$ represent natural language statements meant to be interpreted as first-order propositions in which $x$ (and possibly other variables) occurs free. I'll use $\mathbf\Phi$ and $\mathbf\Psi$ (bold-face) to represent the natural language statements, and $\Phi$ and $\Psi$ (light-face) to represent the corresponding formal statements. So, the first-order proposition you're trying to prove is $\forall x. \Phi(x) \rightarrow \Psi(x)$. Now, in the System LK, two of the rules you'll use for proving this proposition are $(\mathbf{\forall R})$, which here will take the form:
$$\genfrac{}{}{1pt}{}{\Gamma \vdash \Phi(y) \rightarrow \Psi(y),\Delta}{\Gamma \vdash \forall x.\Phi(x) \rightarrow \Psi(x), \Delta}$$
and $(\mathbf{\rightarrow\kern {-1ex} R})$, which here will take the form:
$$\genfrac{}{}{1pt}{}{\Gamma, \Phi(y) \vdash \Psi(y), \Delta}{\Gamma \vdash \Phi(y) \rightarrow \Psi(y), \Delta}$$
These two deduction steps are what take the place of saying "let".
A: I've got a suggestion for you: Invent a completely new symbol which looks exactly like the word "Let". Then use that symbol instead of "Let". This way your desire to use a special symbol is fulfilled, while anyone seeing it will still immediately know what you mean.
A: I agree with others who advise against using an obscure symbol rather than a simple English word.
However, you asked what symbol to use; you didn't ask whether using it is a good idea.
It seems to me that ...
"Let $x \in A$. Then $x$ has the property ..."
can be replaced by
"$\forall x \in A$, $x$ has the property ..."
So, maybe the symbol $\forall$ will serve your needs (in some situations, at least). It's not as obscure as the symbol you mentioned, but I still think the word "let" is better. Your decision, though.
A: In college, many moons ago, I did all of my linear algebra proofs in symbols ... except let because I didn't know it and neither did my professor but when she saw I had a set of the basic proofs all symbolic except let  proofs  took the task on herself to find out and after consulting with other professors she came back with: ∵ (U-2235)
It is an inverted therefor, ∴ (U-2234), and is very frequently misdocumented as "because". There is no inference implied by the symbol; it is definitional and makes "bookends" of the proof. ∵ x .... ∴ P
∵ x ∈ f(y)
A: Note that both × and · are relatively language-independent notations for multiplication.  One is "Cross Multiplication", the other is "Dot Multiplication"; both devolve to "simple linear multiplication" when being applied to degenerate (i.e. 1 by 1 (by 1 by ...)) matrices, and either will generally be recognized as such by any technical person in a locale that uses Arabic-derived mathematics.  In other words, Western countries and Near-Eastern countries, and most of their former colonies and subject-states - which pretty much covers everything but China (I don't know enough about the impact of the "modernization/westernization/digitization" of communications on their technical notations to comment on them).
Both mean entirely different things when the context is multidimensional matrices, however.  That is, in fact, WHY specific symbols are used.  If you just say "Matrix A times Matrix B", it is not clear whether you mean cross-multiplication or dot-multiplication - or even something else entirely.  Sure, there are conventions for ad-hoc interpretation; but for a precise and unambiguous statement, a narrowly-defined (and thus, of restricted use) symbolic language is required.
