Theorem e2ebindALT

Description: Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		axc11n	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑦 𝑦 = 𝑥 )
2		nfe1	⊢ Ⅎ 𝑦 ∃ 𝑦 𝜑
3	2	19.9	⊢ ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 )
4		excom	⊢ ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 )
5		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝑦 = 𝑥
6		id	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑦 𝑦 = 𝑥 )
7		biid	⊢ ( 𝜑 ↔ 𝜑 )
8	7	a1i	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜑 ) )
9	8	drex1	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 𝜑 ↔ ∃ 𝑥 𝜑 ) )
10	6 9	syl	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 𝜑 ↔ ∃ 𝑥 𝜑 ) )
11	5 10	alrimi	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑦 ( ∃ 𝑦 𝜑 ↔ ∃ 𝑥 𝜑 ) )
12		exbi	⊢ ( ∀ 𝑦 ( ∃ 𝑦 𝜑 ↔ ∃ 𝑥 𝜑 ) → ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 𝜑 ) )
13	11 12	syl	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 𝜑 ) )
14		bitr	⊢ ( ( ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 𝜑 ) ∧ ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) ) → ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) )
15	14	ex	⊢ ( ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 𝜑 ) → ( ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) → ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) ) )
16	15	impcom	⊢ ( ( ( ∃ 𝑦 ∃ 𝑥 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) ∧ ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 ∃ 𝑥 𝜑 ) ) → ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) )
17	4 13 16	sylancr	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) )
18		bitr3	⊢ ( ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) → ( ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) → ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) ) )
19	18	impcom	⊢ ( ( ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) ∧ ( ∃ 𝑦 ∃ 𝑦 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) ) → ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) )
20	3 17 19	sylancr	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) )
21	1 20	syl	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑦 𝜑 ) )