Axiom of Specification from Replacement and Empty Set

== Theorem ==
The is a consequence of:
:the 
and
:the .
== Outline of Proof ==
Take some set $A$ and some propositional function $\map P x$.
We obtain the set:
:$ B = \set {x \in A : \map P x}$
by defining the mapping:
:$\map f x = \begin{cases}
x & : \map P x \\
w & : \text{otherwise}
\end{cases}$
on $A$, where we choose some fixed $w \in A : \map P w$.
We obtain its image with the .
This mapping maps all of the $x \in A$ that fulfill $\map P x$ to themselves, ensuring that they are in the image.
It redirects the elements that don't fulfill $\map P x$ to some fixed $w$ that does fulfill $\map P x$.
Thus, the image we have obtained is $B$.
We must also deal with the special case where no elements in $A$ fulfill $\map P x$.
We must map all elements to something to fulfill the mapping definition.
All elements need to be redirected to a $w$ that fulfills $\map P x$, but here, there is no such $w$.
However, the provides us with the desired set.
Thus, we can produce the set $B$ both when it is empty and when it is non-empty.
While this proof outline would suffice as a proof, the construction of set-theoretic mappings relies on Cartesian Product Exists and is Unique, which relies on , making such a proof circular in this context.
We thus must define a propositional function that is not set theoretic to act as the above $f$, leading to a proof that is conceptually the same, but more tedious.
== Proof ==
Let $A$ be an arbitrary set.
Let $\map P x$ be an arbitrary propositional function.
It is to be shown that there exists a set $B$ consisting of exactly the $y \in A$ such that $\map P y$.
That is:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
By Law of Excluded Middle, there are two choices:
:$\exists y \in A : \map P y$
or:
:$\not \exists y \in A : \map P y$
Suppose $\not \exists y \in A : \map P x$.
By , take $B = \O$.
Take arbitrary $A$ and $y$.
Assume $y \in B$.
This contradicts the empty set definition.
By Rule of Explosion, we have:
:$y \in A \land \map P y$
giving:
:$y \in B \implies \paren {y \in A \land \map P y}$
Now assume:
:$y \in A \land \map P y$
This contradicts our assumption that:
:$\not \exists y \in A : \map P y$
By Rule of Explosion, we have:
:$y \in B$
giving:
:$\paren {y \in A \land \map P y} \implies y \in B$
Thus:
:$\paren {y \in A \land \map P y} \iff y \in B$
and by Universal Generalisation and Existential Generalisation:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
This shows that the holds when:
:$\not \exists y \in A : \map P y$
Suppose $\exists y \in A : \map P y$.
Take some fixed $w \in A : \map P w$.
Define the propositional function $\map Q {x, z}$ as follows:
:$\paren {\map P x \land z = x} \lor \paren {\neg \map P x \land z = w}$
Usually this would be written as the mapping:
:$\map f x = \begin {cases}
x & : \map P x \\
w & : \text{otherwise}
\end {cases}$
It is to be shown that $\map Q {x, z}$ determines a mapping.
That is:
:$\forall x: \exists a: \forall z: \paren {\map Q {x, z} \iff a = z}$
Take arbitrary $x$ and $z$.
Assume that $\map Q {x, z}$, giving:
:$\paren {\map P x \land z = x} \lor \paren {\neg \map P x \land z = w}$
By Law of Excluded Middle, there are two choices:
:$\map P x$
or:
:$\neg \map P x$
Suppose $\map P x$.
 that:
:$\paren {\neg \map P x \land z = w}$
Then we have the contradiction:
:$\map P x \land \neg \map P x$
Thus we have:
:$\neg \paren{\neg \map P x \land z = w}$
and by Modus Tollendo Ponens:
:$\paren {\map P x \land z = x}$
Take $a=x$.
Thus, for all $z$ such that $\map Q {x, z}$, we have $a = x = z$, giving:
:$\map Q {x, z} \implies a = z$
Suppose $\neg \map P x$.
 that:
:$\paren {\map P x \land z = x}$
Then we have the contradiction:
:$\map P x \land \neg \map P x$
Thus we have:
:$\neg \paren {\map P x \land z = x}$
and by Modus Tollendo Ponens:
:$\paren {\neg \map P x \land z = w}$
Take $a=w$.
Thus, for all $z$ such that $\map Q {x, z}$, we have $a = w = z$, giving:
:$\map Q {x, z} \implies a = z$
Thus:
:$\map Q {x, z} \implies a = z$
follows from both $\map P x$ and $\neg \map P x$.
By Universal Generalisation and Existential Generalisation:
:$\forall x: \exists a: \forall z: \paren {\map Q {x, z} \iff a = z}$
and $\map Q {x, y}$ determines a mapping.
We now have a propositional function $\map Q {x, y}$ satisfying the premise of , giving:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \exists x \in A : \map Q {x, y} }$
By definition of $\map Q {x, y}$, we have:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \exists x \in A : \paren {\paren {\map P x \land y = x} \lor \paren {\neg \map P x \land y = w} } }$
where $w \in A$ and $\map P w$.
We must show that the holds:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
Assume $y \in B$.
By the , we have:
:$\paren {\map P x \land y = x} \lor \paren {\neg \map P x \land y = w}$
for some $x \in A$.
$\map P x \land y = x$ and $x \in A$ imply $y \in A \land \map P y$.
Recalling that $w \in A$ and $\map P w$, $\neg \map P x \land y = w$ implies $y \in A \land \map P y$.
Thus:
:$y \in B \implies \paren {y \in A \land \map P y}$
Now assume $y \in A \land \map P y$.
Then there is an $x$, namely $x = y$, such that:
:$\exists x \in A : \paren {\map P x \land y = x}$
By Rule of Addition:
:$\exists x \in A : \paren {\paren {\map P x \land y = x} \lor \paren {\neg \map P x \land y = w} }$
Thus, by the we have $y \in B$.
Thus:
:$\paren {y \in A \land \map P y} \implies y \in B$
This completes the biconditional:
:$y \in B \iff \paren {y \in A \land \map P y}$
By Universal Generalisation and Existential Generalisation:
:$\forall A: \exists B: \forall y: \paren {y \in B \iff \paren {y \in A \land \map P y} }$
This shows that the holds when:
:$\exists y \in A : \map P y$
Thus, the holds both when:
:$\exists y \in A : \map P y$
and when:
:$\not \exists y \in A : \map P y$
completing the proof.
Category:Zermelo-Fraenkel Axioms
Category:Empty Set