Theorem e2ebindVD 41266

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

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 2448	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
2		hba1 2301	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦∀𝑦 𝑦 = 𝑥)
3		idn1 40928	. . . . . . . 8 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦 𝑦 = 𝑥   )
4		biid 263	. . . . . . . . . 10 ⊢ (𝜑 ↔ 𝜑)
5	4	a1i 11	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
6	5	drex1 2463	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑))
7	3, 6	e1a 40981	. . . . . . 7 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
8	2, 7	gen11nv 40971	. . . . . 6 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
9		exbi 1847	. . . . . 6 ⊢ (∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑))
10	8, 9	e1a 40981	. . . . 5 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)   )
11		excom 2169	. . . . 5 ⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
12		bibi1 354	. . . . . 6 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) ↔ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)))
13	12	biimprd 250	. . . . 5 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)))
14	10, 11, 13	e10 41048	. . . 4 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)   )
15		nfe1 2154	. . . . 5 ⊢ Ⅎ𝑦∃𝑦𝜑
16	15	19.9 2205	. . . 4 ⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
17		bitr3 355	. . . 4 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)))
18	14, 16, 17	e10 41048	. . 3 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)   )
19	18	in1 40925	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))
20	1, 19	syl 17	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   = wceq 1537  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-10 2145  ax-11 2161  ax-12 2177  ax-13 2390

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-nf 1785  df-vd1 40924

This theorem is referenced by: (None)