Metamath Proof Explorer


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 𝑦 𝜑
Assertion sb8euv ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sb8euv.nf 𝑦 𝜑
2 1 nfsbv 𝑦 [ 𝑤 / 𝑥 ] 𝜑
3 2 sb8eulem ( ∃! 𝑥 𝜑 ↔ ∃! 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )