A question about elements of sets If $x$ is a set and $y\in x$, will it imply $y$ is a set?
Can we prove it using just axioms of Set theory and formal proof system?
If we add this as axiom in Axiom of Set theory, will new axiom system be inconsistent because of Lowernheim Skolem theory? (as there will not any countable model of such axiom system then)
Where by proving element of set is set, I mean to prove $(\forall x)(\forall y)((\exists z)(z=x)\longrightarrow(\exists l)(l=y))$

You seem to be assuming that the language of ZF includes a special sort for "sets" - so that there is a distinction between "set variables" and "general variables." This is a feature of some set theories with urelements, but not of ZF: there is only one kind of "object" (syntactically speaking, only one kind of variable) in ZF. 
This means that a formula like "$(\forall x)(\exists z)(x=z)$" is a tautology (= provable from no axioms at all) - just take $x=z$. If we had a language with sorts, then things would be more interesting: the sentence $$(\forall x^\sigma)(\exists z^\tau )(x=z),$$ asserting that every thing of type $\sigma$ is also a thing of type $\tau$, is definitely not a tautology. (Actually, the opposite may be true: most presentations of many-sorted logic demand that the sorts be distinct! But that's a minor point here.)
