Theorem exsb

An equivalent expression for existence. One direction ( exsbim) needs fewer axioms. (Contributed by NM, 2-Feb-2005.) Avoid [ax-13]. (Revised by Wolf Lammen, 16-Oct-2022.)

Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \)
Proof
l0
nfv
l1
nfa1
l2
ax12v
sp
com12 _
impbid l2 _
cbvexv1 l0 l1 _