Theorem nfald2
Variation on nfald which adds the hypothesis that \( x \) and \( y \) are
distinct in the inner subproof. (Contributed by Mario Carneiro,
8-Oct-2016.) Usage of this theorem is discouraged because it depends on
[ax-13]. Use nfald instead. (New usage is discouraged.)
Hypotheses
nfald2.1
\( \vdash \Finv y \, \varphi \)
nfald2.2
\( \vdash \varphi \wedge \neg \forall x \, x = y \rightarrow \Finv x \, \psi \)
Conclusion
\( \vdash \varphi \rightarrow \Finv x \, \forall y \, \psi \)
Proof
l0
nfald2.1
l1
hbnaev
\( \vdash \neg \forall x \, x = y \rightarrow \forall y \, \neg \forall x \, x = y \)
l2
nf5i _
l3
nfan l0 _
l4
nfald2.2
l5
nfald l3 _
l6
ex _
l7
cbvaev
\( \vdash \forall x \, x = y \rightarrow \forall w \, w = y \)
l8
axc16nf
\( \vdash \forall w \, w = y \rightarrow \Finv x \, \forall y \, \psi \)
l9
syl l7 _
l10
pm2.61d2 l6 _