Metamath Proof Explorer


Theorem sb1v

Description: One direction of sb5 , provable from fewer axioms. Version of sb1 with a disjoint variable condition using fewer axioms. (Contributed by NM, 13-May-1993) (Revised by Wolf Lammen, 20-Jan-2024)

Ref Expression
Assertion sb1v ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) )

Proof

Step Hyp Ref Expression
1 sb6 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) )
2 equs4v ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) )
3 1 2 sylbi ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦𝜑 ) )