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

Metamath Proof Explorer

Theorem gencbvex

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996) (Proof shortened by Andrew Salmon, 8-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 gencbvex.1 ⊢ A ∈ V
2 gencbvex.2 ⊢ A = y → φ ↔ ψ
3 gencbvex.3 ⊢ A = y → χ ↔ θ
4 gencbvex.4 ⊢ θ ↔ ∃ x χ ∧ A = y
5 excom ⊢ ∃ x ∃ y y = A ∧ θ ∧ ψ ↔ ∃ y ∃ x y = A ∧ θ ∧ ψ
6 3 2 anbi12d ⊢ A = y → χ ∧ φ ↔ θ ∧ ψ
7 6 bicomd ⊢ A = y → θ ∧ ψ ↔ χ ∧ φ
8 7 eqcoms ⊢ y = A → θ ∧ ψ ↔ χ ∧ φ
9 1 8 ceqsexv ⊢ ∃ y y = A ∧ θ ∧ ψ ↔ χ ∧ φ
10 9 exbii ⊢ ∃ x ∃ y y = A ∧ θ ∧ ψ ↔ ∃ x χ ∧ φ
11 19.41v ⊢ ∃ x y = A ∧ θ ∧ ψ ↔ ∃ x y = A ∧ θ ∧ ψ
12 simpr ⊢ ∃ x y = A ∧ θ ∧ ψ → θ ∧ ψ
13 eqcom ⊢ A = y ↔ y = A
14 13 biimpi ⊢ A = y → y = A
15 14 adantl ⊢ χ ∧ A = y → y = A
16 15 eximi ⊢ ∃ x χ ∧ A = y → ∃ x y = A
17 4 16 sylbi ⊢ θ → ∃ x y = A
18 17 adantr ⊢ θ ∧ ψ → ∃ x y = A
19 18 ancri ⊢ θ ∧ ψ → ∃ x y = A ∧ θ ∧ ψ
20 12 19 impbii ⊢ ∃ x y = A ∧ θ ∧ ψ ↔ θ ∧ ψ
21 11 20 bitri ⊢ ∃ x y = A ∧ θ ∧ ψ ↔ θ ∧ ψ
22 21 exbii ⊢ ∃ y ∃ x y = A ∧ θ ∧ ψ ↔ ∃ y θ ∧ ψ
23 5 10 22 3bitr3i ⊢ ∃ x χ ∧ φ ↔ ∃ y θ ∧ ψ