Theorem nfe1

The setvar \( x \) is not free in \( \exists x \, \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.)

Conclusion

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

Proof

hbe1

nf5i _