Theorem gencbvex2

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

	Ref	Expression
Hypotheses	gencbvex2.1	$$⊢A\in \mathrm{V}$$
	gencbvex2.2	$$⊢A=y\to \left(\phi \leftrightarrow \psi \right)$$
	gencbvex2.3	$$⊢A=y\to \left(\chi \leftrightarrow \theta \right)$$
	gencbvex2.4	$$⊢\theta \to \exists x\left(\chi \wedge A=y\right)$$
Assertion	gencbvex2	$$⊢\exists x\left(\chi \wedge \phi \right)\leftrightarrow \exists y\left(\theta \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		gencbvex2.1	$$⊢A\in \mathrm{V}$$
2		gencbvex2.2	$$⊢A=y\to \left(\phi \leftrightarrow \psi \right)$$
3		gencbvex2.3	$$⊢A=y\to \left(\chi \leftrightarrow \theta \right)$$
4		gencbvex2.4	$$⊢\theta \to \exists x\left(\chi \wedge A=y\right)$$
5	3	biimpac	$$⊢\left(\chi \wedge A=y\right)\to \theta$$
6	5	exlimiv	$$⊢\exists x\left(\chi \wedge A=y\right)\to \theta$$
7	4 6	impbii	$$⊢\theta \leftrightarrow \exists x\left(\chi \wedge A=y\right)$$
8	1 2 3 7	gencbvex	$$⊢\exists x\left(\chi \wedge \phi \right)\leftrightarrow \exists y\left(\theta \wedge \psi \right)$$