Is the $\in$ relation a dyadic, or a monadic, relation? I believe that it's true (correct me if I'm wrong) that 


*

*When we predicate something of an argument we're saying that that argument is a member of a set intensionally defined just by that predicate?  (I.e. '$Px$' := '$x\in P$ ')

*The $P$ in $Px$ is a monadic relation. 

*The '$\in$' in '$x\in P$ ' is a dyadic relation. 


It seems strange that the two expressions use different relations despite denoting the same thing. I suspect I'm wrong about one of the three points I listed above. Is there anything that I misbelieve? 
 A: In the "pure" language of predicate logic (or FOL) there is no symbol $\in$.
The usual "restricted quantifier" symbol : $(\forall x \in A) \ P(x)$ is an abbreviation for :

$\forall x \ (A(x) \to P(x))$.

When we use it for the first-order language of set theory we need only one predicate symbol, the binary $\in$.
With it we can build atomic formulae, like : $x \in y$, and sentences, like : $\exists x \forall y \lnot (y \in x)$.

The (not trivial) difference is that in "pure" first-order language the expression $P(x)$ is formed with an individual variable symbol : $x$ and a unary (monadic) predicate symbol : $P$.
In the first-order language of set theory, the expression $x \in y$ is formed with two individual variable symbols : $x$ and $y$, and a binary (dyadic) predicate symbol : $\in$.

The "link" between $P(x)$ and $x \in P$ is thorugh the semantics; when we specify an interpretation $\mathcal I$ with domain $D$ for the language, we have to interpret the predicate symbol $P$ with a subset $P^D$ of the domain, i.e. $P^D \subseteq D$.
This interpretation assign a meaning to the atomic formula $P(x)$ throug a variable assignment function :

$s : Var \to D$

i.e. a function mapping individual variables to elements of the domain $D$.
The semantic specification for $P(x)$ will be :

$P(x)$ is satisfied in $\mathcal I$ with $s$ (in symbols : $\mathcal I,s \vDash P(x)$) iff $s(x) \in P^D$. 

