The Lefschetz principle was formulated and illustrated the first time in:
S. Lefschetz, Algebraic Geometry, Princeton University Press, 1953.
The basic idea is that every equation over some algebraically closed field of characteristic $0$ only involves finitely many elements, which generate a subfield isomorphic to a subfield of $\mathbb{C}$. But as Seidenberg points out in
A. Seidenberg, Comments on Lefschetz's principle, American American Monthly (65), No. 9, Nov. 1958, 685 - 690
Lefschetz has not given a rigorous proof and it is not clear at all if it holds when analytical methods over $\mathbb{C}$ are used. Tarski's classical result that the theory of algebraically closed fields of characteristic $0$ admits quantifier elimination and therefore all models are elementary equivalent is called the "Minor Lefschetz principle", because it does not apply to prominent examples such as Hilbert's Nullstellensatz.
A precise formulation, with a short proof, which works in every characteristic, can be found here:
Paul C. Eklof, Lefschetz's Principle and Local Functors, Proc. AMS (37), Nr. 2, Feb. 1973, online
In the language of that paper, the principle states the following: Let $F$ be a functor from universal domains of characteristic $p$ ( = algebraically closed field of infinite transcendence degree over $\mathbb{F}_p$) to some category of many-sorted structures with embeddings, which satisfies the following finiteness condition: If $K \subseteq L$ is an extension, then every finite subset of $F(L)$ is already included in the image of a subextension of finite transcendence degree over $K$.
Then, for all $K,L$, we have that $F(K)$ and $F(L)$ are elementary equivalent.
For a specific statement one wants to prove using the Lefschetz princple, one can take $F(K)$ to be the collection of all "relevant algebraic geometry over $K$".
A generalization is treated in:
Gerhard Frey, Hans-Georg Rück, The strong Lefschetz Principle in Algebraic Geometry, manuscripta math. (55), 385 - 401 (1986)
