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	$$⊢\left[y/x\right]\phi \to \exists x\left(x=y\wedge \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sb6	$$⊢\left[y/x\right]\phi \leftrightarrow \forall x\left(x=y\to \phi \right)$$
2		equs4v	$$⊢\forall x\left(x=y\to \phi \right)\to \exists x\left(x=y\wedge \phi \right)$$
3	1 2	sylbi	$$⊢\left[y/x\right]\phi \to \exists x\left(x=y\wedge \phi \right)$$