Theorem bj-cbvexivw 32660

Description: Change bound variable. This is to cbvexvw 1970 what cbvalivw 1934 is to cbvalvw 1969. [TODO: move after cbvalivw 1934]. (Contributed by BJ, 17-Mar-2020.)

Hypothesis

Ref	Expression
bj-cbvexivw.1	|- ( y = x -> ( ph -> ps ) )

Assertion

Ref	Expression
bj-cbvexivw	|- ( E. x ph -> E. y ps )

Distinct variable groups:   x, y   ps, x   ph, y

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem bj-cbvexivw

Step	Hyp	Ref	Expression
1		ax5e 1841	. 2 |- ( E. x E. y ps -> E. y ps )
2		ax-5 1839	. 2 |- ( ph -> A. y ph )
3		bj-cbvexivw.1	. 2 |- ( y = x -> ( ph -> ps ) )
4	1, 2, 3	bj-cbvexiw 32659	1 |- ( E. x ph -> E. y ps )

Syntax hints:   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by: (None)