Metamath Proof Explorer

Theorem e2ebindVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. e2ebind is e2ebindVD without virtual deductions and was automatically derived from e2ebindVD .

1:: |- ( ph <-> ph )
2:1: |- ( A. y y = x -> ( ph <-> ph ) )
3:2: |- ( A. y y = x -> ( E. y ph <-> E. x ph ) )
4:: |- (. A. y y = x ->. A. y y = x ).
5:3,4: |- (. A. y y = x ->. ( E. y ph <-> E. x ph ) ).
6:: |- ( A. y y = x -> A. y A. y y = x )
7:5,6: |- (. A. y y = x ->. A. y ( E. y ph <-> E. x ph ) ).
8:7: |- (. A. y y = x ->. ( E. y E. y ph <-> E. y E. x ph ) ).
9:: |- ( E. y E. x ph <-> E. x E. y ph )
10:8,9: |- (. A. y y = x ->. ( E. y E. y ph <-> E. x E. y ph ) ).
11:: |- ( E. y ph -> A. y E. y ph )
12:11: |- ( E. y E. y ph <-> E. y ph )
13:10,12: |- (. A. y y = x ->. ( E. x E. y ph <-> E. y ph ) ).
14:13: |- ( A. y y = x -> ( E. x E. y ph <-> E. y ph ) )
15:: |- ( A. y y = x <-> A. x x = y )
qed:14,15: |- ( A. x x = y -> ( E. x E. y ph <-> E. y ph ) )
(Contributed by Alan Sare, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 axc11n ⊢ ∀ x x = y → ∀ y y = x
2 hba1 ⊢ ∀ y y = x → ∀ y ∀ y y = x
3 idn1 ⊢ ∀ y y = x → ∀ y y = x
4 biid ⊢ φ ↔ φ
5 4 a1i ⊢ ∀ y y = x → φ ↔ φ
6 5 drex1 ⊢ ∀ y y = x → ∃ y φ ↔ ∃ x φ
7 3 6 e1a ⊢ ∀ y y = x → ∃ y φ ↔ ∃ x φ
8 2 7 gen11nv ⊢ ∀ y y = x → ∀ y ∃ y φ ↔ ∃ x φ
9 exbi ⊢ ∀ y ∃ y φ ↔ ∃ x φ → ∃ y ∃ y φ ↔ ∃ y ∃ x φ
10 8 9 e1a ⊢ ∀ y y = x → ∃ y ∃ y φ ↔ ∃ y ∃ x φ
11 excom ⊢ ∃ y ∃ x φ ↔ ∃ x ∃ y φ
12 bibi1 ⊢ ∃ y ∃ y φ ↔ ∃ y ∃ x φ → ∃ y ∃ y φ ↔ ∃ x ∃ y φ ↔ ∃ y ∃ x φ ↔ ∃ x ∃ y φ
13 12 biimprd ⊢ ∃ y ∃ y φ ↔ ∃ y ∃ x φ → ∃ y ∃ x φ ↔ ∃ x ∃ y φ → ∃ y ∃ y φ ↔ ∃ x ∃ y φ
14 10 11 13 e10 ⊢ ∀ y y = x → ∃ y ∃ y φ ↔ ∃ x ∃ y φ
15 nfe1 ⊢ Ⅎ y ∃ y φ
16 15 19.9 ⊢ ∃ y ∃ y φ ↔ ∃ y φ
17 bitr3 ⊢ ∃ y ∃ y φ ↔ ∃ x ∃ y φ → ∃ y ∃ y φ ↔ ∃ y φ → ∃ x ∃ y φ ↔ ∃ y φ
18 14 16 17 e10 ⊢ ∀ y y = x → ∃ x ∃ y φ ↔ ∃ y φ
19 18 in1 ⊢ ∀ y y = x → ∃ x ∃ y φ ↔ ∃ y φ
20 1 19 syl ⊢ ∀ x x = y → ∃ x ∃ y φ ↔ ∃ y φ