Theorem e2ebindVD 44254

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

1::	⊢ (𝜑 ↔ 𝜑)
2:1:	⊢ (∀𝑦𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
3:2:	⊢ (∀𝑦𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑 ))
4::	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   ∀𝑦𝑦 = 𝑥   )
5:3,4:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑦𝜑 ↔ ∃𝑥 𝜑)   )
6::	⊢ (∀𝑦𝑦 = 𝑥 → ∀𝑦∀𝑦𝑦 = 𝑥)
7:5,6:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
8:7:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)   )
9::	⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
10:8,9:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)   )
11::	⊢ (∃𝑦𝜑 → ∀𝑦∃𝑦𝜑)
12:11:	⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
13:10,12:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)   )
14:13:	⊢ (∀𝑦𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃ 𝑦𝜑))
15::	⊢ (∀𝑦𝑦 = 𝑥 ↔ ∀𝑥𝑥 = 𝑦)
qed:14,15:	⊢ (∀𝑥𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃ 𝑦𝜑))

(Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
e2ebindVD	⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Proof of Theorem e2ebindVD

Step	Hyp	Ref	Expression
1		axc11n 2419	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
2		hba1 2281	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦∀𝑦 𝑦 = 𝑥)
3		idn1 43916	. . . . . . . 8 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦 𝑦 = 𝑥   )
4		biid 261	. . . . . . . . . 10 ⊢ (𝜑 ↔ 𝜑)
5	4	a1i 11	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
6	5	drex1 2434	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑))
7	3, 6	e1a 43969	. . . . . . 7 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
8	2, 7	gen11nv 43959	. . . . . 6 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
9		exbi 1841	. . . . . 6 ⊢ (∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑))
10	8, 9	e1a 43969	. . . . 5 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)   )
11		excom 2154	. . . . 5 ⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
12		bibi1 351	. . . . . 6 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) ↔ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)))
13	12	biimprd 247	. . . . 5 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)))
14	10, 11, 13	e10 44036	. . . 4 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)   )
15		nfe1 2139	. . . . 5 ⊢ Ⅎ𝑦∃𝑦𝜑
16	15	19.9 2190	. . . 4 ⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
17		bitr3 352	. . . 4 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)))
18	14, 16, 17	e10 44036	. . 3 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)   )
19	18	in1 43913	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))
20	1, 19	syl 17	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531   = wceq 1533  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-11 2146  ax-12 2163  ax-13 2365

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-nf 1778  df-vd1 43912

This theorem is referenced by: (None)