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 ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) )

Proof

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