Theorem sbelx

Description: Elimination of substitution. Also see sbel2x . (Contributed by NM, 5-Aug-1993) Avoid ax-13 . (Revised by Wolf Lammen, 6-Aug-2023) Avoid ax-10 . (Revised by Gino Giotto, 20-Aug-2023)

	Ref	Expression
Assertion	sbelx	$$⊢\phi \leftrightarrow \exists x\left(x=y\wedge \left[x/y\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbequ12r	$$⊢x=y\to \left(\left[x/y\right]\phi \leftrightarrow \phi \right)$$
2	1	equsexvw	$$⊢\exists x\left(x=y\wedge \left[x/y\right]\phi \right)\leftrightarrow \phi$$
3	2	bicomi	$$⊢\phi \leftrightarrow \exists x\left(x=y\wedge \left[x/y\right]\phi \right)$$