Theorem sb8euv

Description: 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)

	Ref	Expression
Hypothesis	sb8euv.nf	$$⊢Ⅎy\phi$$
Assertion	sb8euv	$$⊢\exists !x\phi \leftrightarrow \exists !y\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sb8euv.nf	$$⊢Ⅎy\phi$$
2	1	nfsbv	$$⊢Ⅎy\left[w/x\right]\phi$$
3	2	sb8eulem	$$⊢\exists !x\phi \leftrightarrow \exists !y\left[y/x\right]\phi$$