Prove $\exists A:\forall x: \big(\varphi(x)\implies x\in A\big)$ implies $\{x\in A:\varphi(x)\}$ exists and does not depend on $A$

Question

Background: This excersie figured in a former question of mine.

What I'd like to know:

1. Is my proof correct?
2. Are there any simpler proofs for this proposition?

My attempt (Proof).

Suppose $$\exists A:\forall x:\Big(\varphi(x)\implies x\in A\Big)\tag{1}$$ By applyin the schema of comprehension on the set $A$ in $(1)$, $$\exists B: \forall x: \Big(x\in B\iff x\in A \wedge \varphi(x)\Big)\tag{2}$$

where $B=\{x\in A: \varphi(x)\}$. Thus, proving the sought set exists.

To stablish the existing set $B$ does not depend on $A$, let us further assume $$\exists A': \forall x: \Big(\varphi(x)\implies x\in A'\Big) \tag{3}$$ There are two possible cases:

• Case $i)$ Given any sets $x$, whenever $\varphi(x)$ is true then \begin{align*}\varphi(x)&\implies x\in A\wedge x\in A'\tag*{by $(1)$ and $(2)$}\\ &\implies \Big(x\in A\iff x\in A'\Big)\\ &\implies \Big(x\in A\wedge \varphi(x)\iff x\in A'\wedge \varphi(x)\Big)\\ &\implies \{x\in A:\varphi(x)\}=\{x\in A':\varphi(x)\} \end{align*}

• Case $ii)$ For an arbitrary chosen set $x$, if $¬\varphi(x)$ then \begin{align*} ¬\varphi(x)&\implies ¬(x\in A)\wedge ¬(x\in A')\tag*{by $(1)$ and $(2)$}\\ &\implies A=\emptyset=A'\tag*{by uniqueness of $\emptyset$}\\ &\implies (x\in A\iff x\in A')\\ &\implies \{x\in A:\varphi(x)\}=\{x\in A':\varphi(x)\} \end{align*}

Hence, the set $B$ does not depend on $A$.

Answer 1

The latter part of your proof (independence from the choice of $A$) is incorrect.

Consider $\varphi(x)$ to indicate $x\in\{0,1\},$ $A=\{0,1,2\},$ and $A'=\{0,1,3\}.$ Clearly, for $x=2:=\Bigl\{\emptyset,\bigl\{\emptyset\bigr\},\bigl\{\emptyset,\{\emptyset\}\bigl\}\Bigl\},$ we have $\neg\varphi(x).$ However, we cannot conclude that $x\notin A.$ Also, for $x=4,$ we have $\neg\varphi(x),$ but while $x\notin A$ and $x\notin A',$ we cannot conclude that $A=\emptyset=A'.$

Your first case almost completely does the trick, though it's a bit awkward/ambiguous. I would proceed instead as follows. Let $B:=\{x\in A:\varphi(x)\},$ and assume that $A'$ has the property that $\forall x, \varphi(x)\Longrightarrow x\in A'.$ Show that if $x\in B,$ then $x\in A',$ so that $B\subseteq\{x\in A':\varphi(x)\}.$ An analogous argument shows that $B\supseteq\{x\in A':\varphi(x)\},$ completing the proof.