Theorem exsbim

One direction of the equivalence in exsb is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.)

Conclusion

\( \vdash \exists y \, \forall x \, (x = y \rightarrow \varphi) \rightarrow \exists x \, \varphi \)

Proof

alequexv

exlimiv _