Theorem sb8ef

Substitution of variable in existential quantifier. Version of sb8e with a disjoint variable condition, not requiring [ax-13]. (Contributed by NM, 12-Aug-1993.) (Revised by Wolf Lammen, 19-Jan-2023.)

Hypothesis
sb8f.nf
\( \vdash \Finv y \, \varphi \)
Conclusion
\( \vdash \exists x \, \varphi \leftrightarrow \exists y \, [ y / x ] \, \varphi \)
Proof
l0
sb8f.nf
l1
nfs1v
sbequ12
cbvexv1 l0 l1 _