Theorem
nfexa2
An inner universal quantifier's variable is bound. (Contributed by SN, 11-Feb-2026.)
Conclusion
\( \vdash \Finv x \, \exists y \, \forall x \, \varphi \)
Proof
hbe1a
nfexhe
_
This is the content in the right pane.