First-Order-Logic ZFC It's been the first week at university and we've studied ZFC.
In ZFC, the Axiom schema of specification uses first-order-logic, namely,
$$ \forall A, \mathcal{C}: \exists B: \forall X: ( X \in B \iff X \in A \land \mathcal{C}(X)).$$ 
In this case, $\mathcal{C}$ is a predicate (in German it's Prädikat erster Stufe, hopefully that coincides with the English term). Our professor told us that first-order-logic simply uses operators like $\land, \lor, \exists, \forall, \neg$ and so on but it would take long/be difficult to define it exactly.
Is there any easy way to give a concise description of what exactly can be used in $\mathcal{C}$?
 A: The axioms of ZFC are written in first-order logic, though the axiom schemas correspond to infinite families of axioms. As such, I would write your specification axiom more like: 

For each formula $\varphi$ of first-order logic with at most $x$ as a
  free variable, we have the axiom $$\forall A.\exists B.\forall x.\left[x\in B\iff (x\in A \land \varphi)\right]$$

I might make it a bit more explicit with: $$\forall A.\exists B.\forall y.\left[y\in B\iff (y\in A \land \varphi[x\mapsto y])\right]$$ where $\varphi[x\mapsto y]$ means substitute all free occurrences of $x$ with $y$. You'd probably actually want to allow $\varphi$ to have additional free variables though not $A$ or $B$.
One thing to note is that I do not write $\forall \varphi.\dots$ as this is not allowed in first-order logic. It also doesn't accurately capture what is going on. The "for each formula $\varphi$" is happening meta-logically. That is, we are specifying a procedure for producing an axiom given (the syntax of) a formula.
I assume you are familiar with the syntax of formulas of first-order logic, but if not any resource should list them, e.g. Wikipedia. The exact presentation used (e.g. which symbols are used and what is taken as primitive or derived) may vary, but doesn't have too big an impact and should be specified in whatever textbook you're working from.
