I am puzzled by something regarding variables and equality. Suppose you are in set theory and you know what $x \in A$. Intuitively, we know that this must entail that $\exists y \, (x \in y \wedge y=A)$, right? But how do we prove it? I tried. And here's what I could think.
Basically, I had to introduce some variable $z$ and assume (that's the key word) $z=A$. Then, it was pretty straightforward to derive $x \in z$ $(x \in z \wedge z=A)$ and use existential generalisation to conclude $\exists y \, (x \in y \wedge y=A)$.
However, by the deduction theorem, I have a feeling that all I have proved is $z=A \rightarrow \exists y \, (x \in y \wedge y=A)$
What is the theoretical tool that lets me get rid of $z=A$ and take the consequence as a general fact? Am I allowed to just write $z=A$ in a proof without considering it an assumption? And if so, I wouldn't know which axiom would let me do that.
$x \in A$ --- premise
$A=A$ --- equality axiom
$(x \in A \land A=A)$ --- conjunction-introduction
$\exists y \ (x \in y \land y=A)$ --- $\exists$-introduction.
The $\exists$-introduction rule is:
where $\phi [y/a]$ denotes the operation of substitution, that is, of replacing all free occurrences of $y$ in $\phi$ with a parameter $a$.
In our case, we have $(x \in y \land y=A)$ as $\phi$ and $(x \in A \land A=A)$ as $\phi [y/A]$.