Theorem ax10w

Weak version of [ax-10] from which we can prove any [ax-10] instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. It is an alias of hbn1w introduced for labeling consistency. (Contributed by NM, 9-Apr-2017.) Use hbn1w instead. (New usage is discouraged.)

Hypothesis

ax10w.1

\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)

Conclusion

\( \vdash \neg \forall x \, \varphi \rightarrow \forall x \, \neg \forall x \, \varphi \)

Proof

ax10w.1

\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)

hbn1w _