Metamath Proof Explorer

Theorem e2ebindALT

Description: Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion e2ebindALT ⊢ ∀ x x = y → ∃ x ∃ y φ ↔ ∃ y φ

Proof

Step Hyp Ref Expression
1 axc11n ⊢ ∀ x x = y → ∀ y y = x
2 nfe1 ⊢ Ⅎ y ∃ y φ
3 2 19.9 ⊢ ∃ y ∃ y φ ↔ ∃ y φ
4 excom ⊢ ∃ y ∃ x φ ↔ ∃ x ∃ y φ
5 nfa1 ⊢ Ⅎ y ∀ y y = x
6 id ⊢ ∀ y y = x → ∀ y y = x
7 biid ⊢ φ ↔ φ
8 7 a1i ⊢ ∀ y y = x → φ ↔ φ
9 8 drex1 ⊢ ∀ y y = x → ∃ y φ ↔ ∃ x φ
10 6 9 syl ⊢ ∀ y y = x → ∃ y φ ↔ ∃ x φ
11 5 10 alrimi ⊢ ∀ y y = x → ∀ y ∃ y φ ↔ ∃ x φ
12 exbi ⊢ ∀ y ∃ y φ ↔ ∃ x φ → ∃ y ∃ y φ ↔ ∃ y ∃ x φ
13 11 12 syl ⊢ ∀ y y = x → ∃ y ∃ y φ ↔ ∃ y ∃ x φ
14 bitr ⊢ ∃ y ∃ y φ ↔ ∃ y ∃ x φ ∧ ∃ y ∃ x φ ↔ ∃ x ∃ y φ → ∃ y ∃ y φ ↔ ∃ x ∃ y φ
15 14 ex ⊢ ∃ y ∃ y φ ↔ ∃ y ∃ x φ → ∃ y ∃ x φ ↔ ∃ x ∃ y φ → ∃ y ∃ y φ ↔ ∃ x ∃ y φ
16 15 impcom ⊢ ∃ y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃ y ∃ y φ ↔ ∃ y ∃ x φ → ∃ y ∃ y φ ↔ ∃ x ∃ y φ
17 4 13 16 sylancr ⊢ ∀ y y = x → ∃ y ∃ y φ ↔ ∃ x ∃ y φ
18 bitr3 ⊢ ∃ y ∃ y φ ↔ ∃ x ∃ y φ → ∃ y ∃ y φ ↔ ∃ y φ → ∃ x ∃ y φ ↔ ∃ y φ
19 18 impcom ⊢ ∃ y ∃ y φ ↔ ∃ y φ ∧ ∃ y ∃ y φ ↔ ∃ x ∃ y φ → ∃ x ∃ y φ ↔ ∃ y φ
20 3 17 19 sylancr ⊢ ∀ y y = x → ∃ x ∃ y φ ↔ ∃ y φ
21 1 20 syl ⊢ ∀ x x = y → ∃ x ∃ y φ ↔ ∃ y φ