Theorem cbvexsv

Description: A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	cbvexsv	$$⊢\exists x\phi \leftrightarrow \exists y\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		cbvrexsv	$$⊢\exists x\in \mathrm{V}\phi \leftrightarrow \exists y\in \mathrm{V}\left[y/x\right]\phi$$
2		rexv	$$⊢\exists x\in \mathrm{V}\phi \leftrightarrow \exists x\phi$$
3		rexv	$$⊢\exists y\in \mathrm{V}\left[y/x\right]\phi \leftrightarrow \exists y\left[y/x\right]\phi$$
4	1 2 3	3bitr3i	$$⊢\exists x\phi \leftrightarrow \exists y\left[y/x\right]\phi$$