Metamath Proof Explorer

Theorem spc2ed

Description: Existential specialization with 2 quantifiers, using implicit substitution. (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Hypotheses spc2ed.x ⊢ Ⅎ x χ
spc2ed.y ⊢ Ⅎ y χ
spc2ed.1 ⊢ φ ∧ x = A ∧ y = B → ψ ↔ χ
Assertion spc2ed ⊢ φ ∧ A ∈ V ∧ B ∈ W → χ → ∃ x ∃ y ψ

Proof

Step Hyp Ref Expression
1 spc2ed.x ⊢ Ⅎ x χ
2 spc2ed.y ⊢ Ⅎ y χ
3 spc2ed.1 ⊢ φ ∧ x = A ∧ y = B → ψ ↔ χ
4 elisset ⊢ A ∈ V → ∃ x x = A
5 elisset ⊢ B ∈ W → ∃ y y = B
6 4 5 anim12i ⊢ A ∈ V ∧ B ∈ W → ∃ x x = A ∧ ∃ y y = B
7 exdistrv ⊢ ∃ x ∃ y x = A ∧ y = B ↔ ∃ x x = A ∧ ∃ y y = B
8 6 7 sylibr ⊢ A ∈ V ∧ B ∈ W → ∃ x ∃ y x = A ∧ y = B
9 nfv ⊢ Ⅎ x φ
10 9 1 nfan ⊢ Ⅎ x φ ∧ χ
11 nfv ⊢ Ⅎ y φ
12 11 2 nfan ⊢ Ⅎ y φ ∧ χ
13 anass ⊢ χ ∧ φ ∧ x = A ∧ y = B ↔ χ ∧ φ ∧ x = A ∧ y = B
14 ancom ⊢ χ ∧ φ ↔ φ ∧ χ
15 14 anbi1i ⊢ χ ∧ φ ∧ x = A ∧ y = B ↔ φ ∧ χ ∧ x = A ∧ y = B
16 13 15 bitr3i ⊢ χ ∧ φ ∧ x = A ∧ y = B ↔ φ ∧ χ ∧ x = A ∧ y = B
17 3 biimparc ⊢ χ ∧ φ ∧ x = A ∧ y = B → ψ
18 16 17 sylbir ⊢ φ ∧ χ ∧ x = A ∧ y = B → ψ
19 18 ex ⊢ φ ∧ χ → x = A ∧ y = B → ψ
20 12 19 eximd ⊢ φ ∧ χ → ∃ y x = A ∧ y = B → ∃ y ψ
21 10 20 eximd ⊢ φ ∧ χ → ∃ x ∃ y x = A ∧ y = B → ∃ x ∃ y ψ
22 21 impancom ⊢ φ ∧ ∃ x ∃ y x = A ∧ y = B → χ → ∃ x ∃ y ψ
23 8 22 sylan2 ⊢ φ ∧ A ∈ V ∧ B ∈ W → χ → ∃ x ∃ y ψ