Theorem ax6ev

At least one individual exists. Weaker version of ax6e. When possible, use of this theorem rather than ax6e is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.)

Conclusion
\( \vdash \exists x \, x = y' \)
Proof
l0
ax6v
\( \vdash \neg \forall x \, \neg x = y' \)
df-ex
\( \vdash \exists x \, x = y' \leftrightarrow \neg \forall x \, \neg x = y' \)
mpbir l0 _