Theorem exexw

Existential quantification over a given variable is idempotent. Weak version of [bj-exexbiex], requiring fewer axioms. (Contributed by GG, 4-Nov-2024.)

Hypothesis
exexw.1
\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists x \, \exists x \, \varphi \)
Proof
l0
19.9v
l1
bicomi _