Theorem e2ebindVD 45988

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

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 2455	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
2		hba1 2326	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦∀𝑦 𝑦 = 𝑥)
3		idn1 45651	. . . . . . . 8 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦 𝑦 = 𝑥   )
4		biid 264	. . . . . . . . . 10 ⊢ (𝜑 ↔ 𝜑)
5	4	a1i 11	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
6	5	drex1 2470	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑))
7	3, 6	e1a 45704	. . . . . . 7 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
8	2, 7	gen11nv 45694	. . . . . 6 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
9		exbi 1879	. . . . . 6 ⊢ (∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑))
10	8, 9	e1a 45704	. . . . 5 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)   )
11		excom 2198	. . . . 5 ⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
12		bibi1 354	. . . . . 6 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) ↔ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)))
13	12	biimprd 251	. . . . 5 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑) → ((∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑) → (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)))
14	10, 11, 13	e10 45771	. . . 4 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)   )
15		nfe1 2186	. . . . 5 ⊢ Ⅎ𝑦∃𝑦𝜑
16	15	19.9 2241	. . . 4 ⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
17		bitr3 355	. . . 4 ⊢ ((∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑) → ((∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑) → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)))
18	14, 16, 17	e10 45771	. . 3 ⊢ (   ∀𝑦 𝑦 = 𝑥   ▶   (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)   )
19	18	in1 45648	. 2 ⊢ (∀𝑦 𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))
20	1, 19	syl 18	1 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-nf 1816  df-vd1 45647

This theorem is used by: (None)