Theorem axc16nf

If [dtru] is false, then there is only one element in the universe, so everything satisfies F/. (Contributed by Mario Carneiro, 7-Oct-2016.) Remove dependency on [ax-11]. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on [ax-10]. (Revised by Wolf Lammen, 12-Oct-2021.)

Conclusion
\( \vdash \forall x \, x = y' \rightarrow \Finv z \, \varphi \)
Proof
l0
axc16g
\( \vdash \forall x \, x = y' \rightarrow \neg \varphi \rightarrow \forall z \, \neg \varphi \)
eximal
\( \vdash \exists z \, \varphi \rightarrow \varphi \leftrightarrow \neg \varphi \rightarrow \forall z \, \neg \varphi \)
l2
sylibr l0 _
\( \vdash \forall x \, x = y' \rightarrow \exists z \, \varphi \rightarrow \varphi \)
axc16g
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall z \, \varphi \)
syld l2 _
nfd _