Theorem gencbvex2

Description: Restatement of gencbvex with weaker hypotheses. (Contributed by Jeff Hankins, 6-Dec-2006)

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

Proof

Step	Hyp	Ref	Expression
1		gencbvex2.1	|- A e. _V
2		gencbvex2.2	|- ( A = y -> ( ph <-> ps ) )
3		gencbvex2.3	|- ( A = y -> ( ch <-> th ) )
4		gencbvex2.4	|- ( th -> E. x ( ch /\ A = y ) )
5	3	biimpac	|- ( ( ch /\ A = y ) -> th )
6	5	exlimiv	|- ( E. x ( ch /\ A = y ) -> th )
7	4 6	impbii	|- ( th <-> E. x ( ch /\ A = y ) )
8	1 2 3 7	gencbvex	|- ( E. x ( ch /\ ph ) <-> E. y ( th /\ ps ) )