Theorem gencbvex

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Hypotheses	gencbvex.1	|- A e. _V
	gencbvex.2	|- ( A = y -> ( ph <-> ps ) )
	gencbvex.3	|- ( A = y -> ( ch <-> th ) )
	gencbvex.4	|- ( th <-> E. x ( ch /\ A = y ) )
Assertion	gencbvex	|- ( E. x ( ch /\ ph ) <-> E. y ( th /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		gencbvex.1	|- A e. _V
2		gencbvex.2	|- ( A = y -> ( ph <-> ps ) )
3		gencbvex.3	|- ( A = y -> ( ch <-> th ) )
4		gencbvex.4	|- ( th <-> E. x ( ch /\ A = y ) )
5		excom	|- ( E. x E. y ( y = A /\ ( th /\ ps ) ) <-> E. y E. x ( y = A /\ ( th /\ ps ) ) )
6	3 2	anbi12d	|- ( A = y -> ( ( ch /\ ph ) <-> ( th /\ ps ) ) )
7	6	bicomd	|- ( A = y -> ( ( th /\ ps ) <-> ( ch /\ ph ) ) )
8	7	eqcoms	|- ( y = A -> ( ( th /\ ps ) <-> ( ch /\ ph ) ) )
9	1 8	ceqsexv	|- ( E. y ( y = A /\ ( th /\ ps ) ) <-> ( ch /\ ph ) )
10	9	exbii	|- ( E. x E. y ( y = A /\ ( th /\ ps ) ) <-> E. x ( ch /\ ph ) )
11		19.41v	|- ( E. x ( y = A /\ ( th /\ ps ) ) <-> ( E. x y = A /\ ( th /\ ps ) ) )
12		simpr	|- ( ( E. x y = A /\ ( th /\ ps ) ) -> ( th /\ ps ) )
13		eqcom	|- ( A = y <-> y = A )
14	13	biimpi	|- ( A = y -> y = A )
15	14	adantl	|- ( ( ch /\ A = y ) -> y = A )
16	15	eximi	|- ( E. x ( ch /\ A = y ) -> E. x y = A )
17	4 16	sylbi	|- ( th -> E. x y = A )
18	17	adantr	|- ( ( th /\ ps ) -> E. x y = A )
19	18	ancri	|- ( ( th /\ ps ) -> ( E. x y = A /\ ( th /\ ps ) ) )
20	12 19	impbii	|- ( ( E. x y = A /\ ( th /\ ps ) ) <-> ( th /\ ps ) )
21	11 20	bitri	|- ( E. x ( y = A /\ ( th /\ ps ) ) <-> ( th /\ ps ) )
22	21	exbii	|- ( E. y E. x ( y = A /\ ( th /\ ps ) ) <-> E. y ( th /\ ps ) )
23	5 10 22	3bitr3i	|- ( E. x ( ch /\ ph ) <-> E. y ( th /\ ps ) )