how to represent the predicate member/2 in first order logic? Lets say we have a predicate that returns true if there is a member in a list. False if not. In prolog I ended up with a code like below
member(B,[B|_]).
member(B,[_|A]):- member(B,A).

Its true for member(1,[3,1,2]). and false for member(1,[4,5,6]). How to use FOL to represent the above function?
 A: In first order logic you might want to use a predicate and not a function to represent your function. If $F$ is a $n$-ary function in a FOL, then if $X_1,\ldots,X_n$ are terms of your language $F(X_1,\ldots,X_n)$ will again be a term. For example, $+(X_1,X_2) \colon = X_1+X_2$ represents the sum function in PA.
Now, $X_1 \in X_2$ is not a term! It's a first-order formula (a thing that you want to put a truth value). When you want $F(X_1,\ldots,X_n)$ to represent a formula (and receive a truth value), then $F$ must be a predicate symbol.
In your case, member$(X_1,X_2) \colon = X_1 \in X_2$ 
A: First of all, given a formula $\varphi$, a term $t$ and a variable $x$, let $\varphi[x\gets t]$ denote a substitution instance, that is the result of $t$ substituted for $x$ in $\varphi$. (*) 
To introduce membership, first  one needs to introduce classes, which are special FOL terms.
Given the formula $\varphi$ and the variable $x$, let the string
$$\{x \mid \varphi\}$$
denote a term named class term or simply class.
Given the formulae $\varphi, \psi$ and the variables $x,y,z$ and the term $t$, we set the following abbreviations:
$$
\begin{aligned}
t \in \{x \mid \varphi\} &\quad\text{short for}\quad \varphi[x \gets t]\\
%
\{x \mid \varphi\} \in t &\quad\text{short for}\quad  
\exists z ( (z \in t) \wedge \forall x ((x\in z) \leftrightarrow \varphi))\\
%
\{x \mid \varphi\} \in \{y \mid \psi\}  &\quad\text{short for}\quad  
\exists z (\psi[y \gets z] \wedge \forall x ((x\in z) \leftrightarrow \varphi))
\end{aligned}
$$
where $\in$ denotes the membership predicate.
(*)
Note that syntactic substitution is a formal FOL operation and not a mere find-and-replace. Particularly, one should introduce  fresh variables when substitution terms are bound variables in their formulae.
