Theorem sb8euv

Variable substitution in unique existential quantifier. Version of sb8eu requiring more disjoint variables, but fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Wolf Lammen, 7-Feb-2023.)

Hypothesis

sb8euv.nf

\( \vdash \Finv y \, \varphi \)

Conclusion

\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, [ y / x ] \, \varphi \)

Proof

sb8euv.nf

nfsbv _

\( \vdash \Finv y \, [ w / x ] \, \varphi \)

sb8eulem _