Theorem 19.8v

Version of 19.8a with a disjoint variable condition, requiring fewer axioms. Converse of ax5e. (Contributed by BJ, 12-Mar-2020.)

Conclusion

\( \vdash \varphi \rightarrow \exists x \, \varphi \)

Proof

ax-5

19.8w _