This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gencbvex2

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

Ref Expression
Hypotheses gencbvex2.1 ⊢ A ∈ V
gencbvex2.2 ⊢ A = y → φ ↔ ψ
gencbvex2.3 ⊢ A = y → χ ↔ θ
gencbvex2.4 ⊢ θ → ∃ x χ ∧ A = y
Assertion gencbvex2 ⊢ ∃ x χ ∧ φ ↔ ∃ y θ ∧ ψ

Proof

Step Hyp Ref Expression
1 gencbvex2.1 ⊢ A ∈ V
2 gencbvex2.2 ⊢ A = y → φ ↔ ψ
3 gencbvex2.3 ⊢ A = y → χ ↔ θ
4 gencbvex2.4 ⊢ θ → ∃ x χ ∧ A = y
5 3 biimpac ⊢ χ ∧ A = y → θ
6 5 exlimiv ⊢ ∃ x χ ∧ A = y → θ
7 4 6 impbii ⊢ θ ↔ ∃ x χ ∧ A = y
8 1 2 3 7 gencbvex ⊢ ∃ x χ ∧ φ ↔ ∃ y θ ∧ ψ