Proving a theorem with Equality. This question is from "Introduction to Mathematical Logic" by Elliot Mendelson , page 96 , exercise 2.65(a). I have to prove the following theorem (we are working in a theory with equality):

$\vdash (\forall x)(\mathscr B(x) \leftrightarrow (\exists y)(x = y \land \mathscr B(y)))$ if $y$ does not occur in $\mathscr B(x)$

I guess I have to show that $\vdash (\mathscr B(x) \leftrightarrow (\exists y)(x = y \land \mathscr B(y)))$ and $\vdash (\forall x)(\mathscr B(x) \leftrightarrow (\exists y)(x = y \land \mathscr B(y)))$ follows from that by Gen. So , I have to show that $\vdash (\mathscr B(x) \rightarrow (\exists y)(x = y \land \mathscr B(y)))$ and $\vdash (\mathscr B(x) \leftarrow (\exists y)(x = y \land \mathscr B(y)))$
For the first case:

*

*$\mathscr B(x)$

*$x = x$ [Proposition 2.23(a)]

*$x = x \land \mathscr B(x)$ [conjunction introduction]

*$(\exists y)(x = y \land \mathscr B(y)) $ [rule E4]

*$\mathscr B(x) \vdash (\exists y)(x = y \land \mathscr B(y)) $

*$\vdash \mathscr B(x) \to  (\exists y)(x = y \land \mathscr B(y)) $ [Deduction]

I am stuck on the second case. I cant really use the rule E4 on proving the second case . I also tried to work backwards to find an easier wf I can prove to prove the second case.But that just made the problem harder. Can someone give me a hint?
Just for comparison , I tried to prove exercise 2.65(b) , which only differs from a quantifier.I am not fully sure if my proof is correct or not , but I tried.

$\vdash (\forall x)(\mathscr B(x) \leftrightarrow (\forall y)(x = y \land \mathscr B(y)))$ if $y$ does not occur in $\mathscr B(x)$

Proof:

*

*$\mathscr B(x)$

*$x=y \to (\mathscr B(x) \to \mathscr B(y))$ [axiom A7]

*$\mathscr B(x) \to (x=y \to \mathscr B(y))$

*$x=y \to \mathscr B(y)$

*$(\forall y)(x=y \to \mathscr B(y))$

*$\mathscr B(x) \vdash (\forall y)(x=y \to \mathscr B(y))$

*$\vdash \mathscr B(x) \to (\forall y)(x=y \to \mathscr B(y))$ [deduction]

*$(\forall y)(x=y \to \mathscr B(y))$

*$x=x \to \mathscr B(x)$

*$x=x$ [Proposition 2.23(a)]

*$\mathscr B(x)$

*$(\forall y)(x=y \to \mathscr B(y)) \vdash \mathscr B(x)$

*$\vdash (\forall y)(x=y \to \mathscr B(y)) \to \mathscr B(x)$

*$\vdash \mathscr B(x) \to (\forall y)(x=y \to \mathscr B(y) \land (\forall y)(x=y \to \mathscr B(y)) \to \mathscr B(x)$ [conjunction intorduction]

*$\vdash \mathscr B(x) \leftrightarrow (\forall y)(x=y \to \mathscr B(y))$ [biconditional introduction]

*$\vdash (\forall x)(\mathscr B(x) \leftrightarrow (\forall y)(x=y \to \mathscr B(y)))$ [Gen]

 A: Hint
Use Rule C.
From premise $(∃y)(x=y ∧ B(y))$ we have $(x=b ∧ B(b))$ for some $b$.
Thus, using substitutivity of equality we have $B(x)$.
Thus, $(∃y)(x=y ∧ B(y)) \vdash_C B(x)$ and from Prop.2.10: $(∃y)(x=y ∧ B(y)) \vdash B(x)$.
A: It is easy if you use rule C (existential specification). However,
the exercise is asking for a proof for any logic with equality. So, perhaps rule C is not included. So, you should transform your proof into one that does not use rule C, according with the method which Mendelson provides in page 83. Here is a proof of $\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash_{C}\mathscr{B}(x)$:

*

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)$ (premise)

*$x=\alpha\wedge\mathscr{B}(\alpha)$ (rule c)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha$ (conjunction
elimination)

*$x=\alpha$ (M.P. 3,2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)$
(conjunction elimination)

*$\mathscr{B}(\alpha)$ (M.P. 5,2)

*$x=\alpha\rightarrow\alpha=x$ (property 2.23-b)

*$\alpha=x$ (M.P. 7,4)

*$\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)$ (axiom A7)

*$\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)$ (M.P. 9,8)

*$\mathscr{B}(x)$ (M.P. 10,6)

Now, we transform it into a proof of $\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash\mathscr{B}(x)$:

*

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right),x=\alpha\wedge\mathscr{B}(\alpha)\vdash\mathscr{B}(x)$
(step 2 of the proof became a premise)

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)$
(by deduction theorem)

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash\forall z\left(x=z\wedge\mathscr{B}(z)\rightarrow\mathscr{B}(x)\right)$
(by universal generalization)

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash\exists y\left(x=y\wedge\mathscr{B}(y)\right)\rightarrow\mathscr{B}(x)$
(by exercise 2.32)

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash\exists y\left(x=y\wedge\mathscr{B}(y)\right)$
(tautological)

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)\vdash\mathscr{B}(x)$
I will go further, in order to make it more clear. We evoked the deduction
theorem to go from step 1 to step 2, in the transformation above.
Instead, the proof of the deduction theorem can show us how we can
get there, without using it. We use the following theorems of propositional
logic:

*

*$p\rightarrow p$

*$p\rightarrow\left(q\rightarrow p\right)$

*$\left(p\rightarrow q\right)\rightarrow\left[\left[p\rightarrow\left(q\rightarrow r\right)\right]\rightarrow\left(p\rightarrow r\right)\right]$
After each step $i$ of the proof, we do the following: if the formula
$S_{i}$ of stem $i$ is a premise, an axiom or a theorem, then, we
introduce the formula $S_{i}\rightarrow\left(Q\rightarrow S_{i}\right)$
(theorem 2), where $Q$ is the premise we want to eliminate, and we
use modus ponens. Here, $Q$ is: $x=\alpha\wedge\mathscr{B}(\alpha)$.
If $S_{i}$ is $Q$, we replace it with $Q\rightarrow Q$ (theorem
1). If $S_{i}$ occurred from modus ponens, from formulas $S_{j}$
and $S_{j}\rightarrow S_{i}$, $j<i$, then we already have $Q\rightarrow S_{j}$
and $Q\rightarrow\left(S_{j}\rightarrow S_{i}\right)$. We replace
$S_{i}$ with $\left(Q\rightarrow S_{j}\right)\rightarrow\left[\left[Q\rightarrow\left(S_{j}\rightarrow S_{i}\right)\right]\rightarrow\left(Q\rightarrow S_{1}\right)\right]$
(theorem 3), and apply modus ponens twice. Finally, we have a proof
of $Q\rightarrow R$, where $R$ is the conclusion of our initial
proof. Here, $R$ is $\mathscr{B}(x)$:

*

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)$ (premise)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\wedge\mathscr{B}(\alpha)$ (th. 1)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha$ (conjunction
elimination)

*$\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right)\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right)\right]$
(th. 2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right)$
(M.P. 4,3)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\wedge\mathscr{B}(\alpha)\right]\rightarrow\left(\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right]\right)$
(th. 3)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right]$
(M.P. 6,2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha$ (M.P. 7,5)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)$
(conjunction elimination)

*$\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right)\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right)\right]$
(th. 2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right)$
(M.P. 10,9)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\wedge\mathscr{B}(\alpha)\right]\rightarrow\left(\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right]\right)$
(th. 3)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right]$
(M.P. 12,2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)$
(M.P. 13,11)

*$x=\alpha\rightarrow\alpha=x$ (property 2.23-b)

*$\left(x=\alpha\rightarrow\alpha=x\right)\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\rightarrow\alpha=x\right)\right]$
(th. 2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\rightarrow\alpha=x\right)$ (M.P. 16,15)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow x=\alpha\right]\rightarrow\left(\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\rightarrow\alpha=x\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\alpha=x\right]\right)$
(th. 3)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(x=\alpha\rightarrow\alpha=x\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\alpha=x\right]$
(M.P. 18,8)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\alpha=x$ (M.P. 19,17)

*$\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)$
(axiom A7)

*$\left[\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\rightarrow\left(x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left[\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\right)$
(th. 2)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left[\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]$
(M.P. 22,21)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\alpha=x\right]\rightarrow\left(\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left[\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\right)$
(th. 3)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left[\alpha=x\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]$
(M.P. 24,20)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)$ (M.P. 25,23)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(\alpha)\right]\rightarrow\left(\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right]\right)$
(th. 3)

*$\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\left(\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right)\right]\rightarrow\left[x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)\right]$ (M.P. 27,14)

*$x=\alpha\wedge\mathscr{B}(\alpha)\rightarrow\mathscr{B}(x)$ (M.P. 28,26)

*$\forall z\left(x=z\wedge\mathscr{B}(z)\rightarrow\mathscr{B}(x)\right)$
(Un. Gen. 29)

*$\exists y\left(x=y\wedge\mathscr{B}(y)\right)\rightarrow\mathscr{B}(x)$
(property by exercise 2.32, on 30)

*$\mathscr{B}(x)$ (M.P. 31,1)

A: I seems Mendelson defines $\exists x \, \mathscr B(x)$ as $\neg \forall x \, \neg \mathscr B(x)$ so let's use this definition in the proof.

*

*$(\exists y)( x = y ~\land \mathscr B(y)) \vdash  \mathscr B(x)$

*$\neg (\forall y ) \neg ( x = y ~\land \mathscr B(y)) \vdash \mathscr B(x)~~~~$ [ Definition of $\exists$ ]

*$\neg \mathscr B(x) \vdash(\forall y ) \neg ( x = y ~\land \mathscr B(y))~~~~$ [Contraposition]

*$\neg \mathscr B(x) \vdash \neg ( x = y ~\land \mathscr B(y))~~~~$

*$ x = y ~\land \mathscr B(y) \vdash \mathscr B(x)~~~~$ [Contraposition]

*$~\vdash x = y \rightarrow \mathscr B(y) \rightarrow \mathscr B(x)~~~~$ [A7 (page 95)]


The jump
$1.$ $(\exists y)( x = y ~\land \mathscr B(y)) \vdash  \mathscr B(x)$
$5.$ $ ~~~~~~~~~~x = y ~\land \mathscr B(y) \vdash \mathscr B(x)$
is a useful lemma in general.
