Theorem e2ebindVD 42421

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

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 2426	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
2		hba1 2293	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦∀𝑦 𝑦 = 𝑥)
3		idn1 42083	. . . . . . . 8 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦 𝑦 = 𝑥   )
4		biid 260	. . . . . . . . . 10 ⊢ (𝜑 ↔ 𝜑)
5	4	a1i 11	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
6	5	drex1 2441	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑))
7	3, 6	e1a 42136	. . . . . . 7 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
8	2, 7	gen11nv 42126	. . . . . 6 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
9		exbi 1850	. . . . . 6 ⊢ (∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑))
10	8, 9	e1a 42136	. . . . 5 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)   )
11		excom 2164	. . . . 5 ⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
12		bibi1 351	. . . . . 6 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) ↔ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)))
13	12	biimprd 247	. . . . 5 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)))
14	10, 11, 13	e10 42203	. . . 4 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)   )
15		nfe1 2149	. . . . 5 ⊢ Ⅎ𝑦∃𝑦𝜑
16	15	19.9 2201	. . . 4 ⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
17		bitr3 352	. . . 4 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)))
18	14, 16, 17	e10 42203	. . 3 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)   )
19	18	in1 42080	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))
20	1, 19	syl 17	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539  ∃wex 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173  ax-13 2372

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-vd1 42079

This theorem is referenced by: (None)