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

Metamath Proof Explorer

Theorem spc3egv

Description: Existential specialization with three quantifiers, using implicit substitution. (Contributed by NM, 12-May-2008) Avoid ax-10 and ax-11 . (Revised by GG, 20-Aug-2023) (Proof shortened by Wolf Lammen, 25-Aug-2023)

Ref Expression
Hypothesis spc3egv.1 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
Assertion spc3egv ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ψ → ∃ x ∃ y ∃ z φ

Proof

Step Hyp Ref Expression
1 spc3egv.1 ⊢ x = A ∧ y = B ∧ z = C → φ ↔ ψ
2 elex ⊢ A ∈ V → A ∈ V
3 elex ⊢ B ∈ W → B ∈ V
4 elex ⊢ C ∈ X → C ∈ V
5 simp1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V
6 1 3coml ⊢ y = B ∧ z = C ∧ x = A → φ ↔ ψ
7 6 3expa ⊢ y = B ∧ z = C ∧ x = A → φ ↔ ψ
8 7 pm5.74da ⊢ y = B ∧ z = C → x = A → φ ↔ x = A → ψ
9 8 spc2egv ⊢ B ∈ V ∧ C ∈ V → x = A → ψ → ∃ y ∃ z x = A → φ
10 19.37v ⊢ ∃ z x = A → φ ↔ x = A → ∃ z φ
11 10 exbii ⊢ ∃ y ∃ z x = A → φ ↔ ∃ y x = A → ∃ z φ
12 19.37v ⊢ ∃ y x = A → ∃ z φ ↔ x = A → ∃ y ∃ z φ
13 11 12 bitri ⊢ ∃ y ∃ z x = A → φ ↔ x = A → ∃ y ∃ z φ
14 9 13 imbitrdi ⊢ B ∈ V ∧ C ∈ V → x = A → ψ → x = A → ∃ y ∃ z φ
15 14 pm2.86d ⊢ B ∈ V ∧ C ∈ V → x = A → ψ → ∃ y ∃ z φ
16 15 3adant1 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → x = A → ψ → ∃ y ∃ z φ
17 16 imp ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ x = A → ψ → ∃ y ∃ z φ
18 5 17 spcimedv ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → ψ → ∃ x ∃ y ∃ z φ
19 2 3 4 18 syl3an ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ X → ψ → ∃ x ∃ y ∃ z φ