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	|- ( E. x ph <-> E. y [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		cbvrexsv	|- ( E. x e. _V ph <-> E. y e. _V [ y / x ] ph )
2		rexv	|- ( E. x e. _V ph <-> E. x ph )
3		rexv	|- ( E. y e. _V [ y / x ] ph <-> E. y [ y / x ] ph )
4	1 2 3	3bitr3i	|- ( E. x ph <-> E. y [ y / x ] ph )