Can one prove the Cantor-Bernstein (or Schröder-Bernstein) theorem without using the Axiom of Infinity?



Axiom of Infinity needed in Cantor-Bernstein?
Actually, the usual proof of the Cantor-Schröder-Bernstein Theorem does not use the Axiom of Infinity (nor the Axiom of Powersets). 


By the usual proof, I mean the one found on [Wikipedia](http://en.wikipedia.org/wiki/Cantor%E2%80%93Bernstein%E2%80%93Schroeder_theorem#Proof), for example. Using the notation from that proof, the main point of contention is whether we can form the sets $C\_n$ and $C = \bigcup\_{n=0}^\infty C\_n$. These sets exist by comprehension:


$C\_0 = \{x \in A: \forall y \in B\,(x \neq g(y))\}$


$C\_n = \{x \in A: \exists s\,(s:\{0,\dots,n\}\to A \land s(0) \in C\_0 \land (\forall i < n)(s(i+1) = g(f(s(i)))) \land s(n) = x\}$,


where abbreviations such as $s:\{0,\dots,n\}\to A$ should be replaced by the equivalent (bounded) formulas in the language of set theory. The definition of $C\_n$ is uniform in $n$, and so


$C = \{x \in A: \exists n\,(\mathrm{FinOrd}(n) \land x \in C\_n)\}$,


where $x \in C\_n$ should be replaced by the above definition and $\mathrm{FinOrd}(n)$ is an abbreviation for "$n$ is zero or a successor ordinal and every element of $n$ is zero or a successor ordinal." An alternate definition of $C$ is


$C = \{x \in A: \forall D\,(C\_0 \subseteq D \subseteq A \land g[f[D]] \subseteq D \to x \in D)\}$,


which shows that $C$ is $\Delta\_1$-definable. The rest of the proof uses induction on finite ordinals, but since the definition of the sets $C\_n$ is uniform these are special cases of transfinite induction. 


In conclusion, it looks like the proof could work in [Kripke-Platek Set Theory](http://en.wikipedia.org/wiki/Kripke%E2%80%93Platek_set_theory) — which has neither the Axiom of Infinity nor the Axiom of Powersets — provided that the two definitions of $C$ given above are provably equivalent. I haven't tried to check whether the two definitions are provably equivalent but, in any case, the proof can be carried out in Kripke-Platek Set Theory with $\Sigma\_1$-Comprehension.


