Theorem gencbvex2

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

	Ref	Expression
Hypotheses	gencbvex2.1	⊢ 𝐴 ∈ V
	gencbvex2.2	⊢ ( 𝐴 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	gencbvex2.3	⊢ ( 𝐴 = 𝑦 → ( 𝜒 ↔ 𝜃 ) )
	gencbvex2.4	⊢ ( 𝜃 → ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
Assertion	gencbvex2	⊢ ( ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝜃 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		gencbvex2.1	⊢ 𝐴 ∈ V
2		gencbvex2.2	⊢ ( 𝐴 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		gencbvex2.3	⊢ ( 𝐴 = 𝑦 → ( 𝜒 ↔ 𝜃 ) )
4		gencbvex2.4	⊢ ( 𝜃 → ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
5	3	biimpac	⊢ ( ( 𝜒 ∧ 𝐴 = 𝑦 ) → 𝜃 )
6	5	exlimiv	⊢ ( ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) → 𝜃 )
7	4 6	impbii	⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
8	1 2 3 7	gencbvex	⊢ ( ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝜃 ∧ 𝜓 ) )