Theorem gencbval

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996)

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

Proof

Step	Hyp	Ref	Expression
1		gencbval.1	|- A e. _V
2		gencbval.2	|- ( A = y -> ( ph <-> ps ) )
3		gencbval.3	|- ( A = y -> ( ch <-> th ) )
4		gencbval.4	|- ( th <-> E. x ( ch /\ A = y ) )
5	2	notbid	|- ( A = y -> ( -. ph <-> -. ps ) )
6	1 5 3 4	gencbvex	|- ( E. x ( ch /\ -. ph ) <-> E. y ( th /\ -. ps ) )
7		exanali	|- ( E. x ( ch /\ -. ph ) <-> -. A. x ( ch -> ph ) )
8		exanali	|- ( E. y ( th /\ -. ps ) <-> -. A. y ( th -> ps ) )
9	6 7 8	3bitr3i	|- ( -. A. x ( ch -> ph ) <-> -. A. y ( th -> ps ) )
10	9	con4bii	|- ( A. x ( ch -> ph ) <-> A. y ( th -> ps ) )