Theorem wl-exeq

Description: The semantics of E. x y = z . (Contributed by Wolf Lammen, 27-Apr-2018)

	Ref	Expression
Assertion	wl-exeq	⊢ ( ∃ 𝑥 𝑦 = 𝑧 ↔ ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		nfeqf	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → Ⅎ 𝑥 𝑦 = 𝑧 )
2	1	19.9d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( ∃ 𝑥 𝑦 = 𝑧 → 𝑦 = 𝑧 ) )
3	2	impancom	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∃ 𝑥 𝑦 = 𝑧 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )
4	3	orrd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∃ 𝑥 𝑦 = 𝑧 ) → ( ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
5	4	expcom	⊢ ( ∃ 𝑥 𝑦 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) )
6	5	orrd	⊢ ( ∃ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 ∨ ( ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) )
7		3orass	⊢ ( ( ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ↔ ( ∀ 𝑥 𝑥 = 𝑦 ∨ ( ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) ) )
8	6 7	sylibr	⊢ ( ∃ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
9		3orrot	⊢ ( ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) ↔ ( ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ∨ 𝑦 = 𝑧 ) )
10	8 9	sylibr	⊢ ( ∃ 𝑥 𝑦 = 𝑧 → ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) )
11		19.8a	⊢ ( 𝑦 = 𝑧 → ∃ 𝑥 𝑦 = 𝑧 )
12		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑧
13		ax7	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑧 → 𝑦 = 𝑧 ) )
14	13	com12	⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝑦 → 𝑦 = 𝑧 ) )
15	12 14	eximii	⊢ ∃ 𝑥 ( 𝑥 = 𝑦 → 𝑦 = 𝑧 )
16	15	19.35i	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 𝑦 = 𝑧 )
17		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦
18	17 13	eximii	⊢ ∃ 𝑥 ( 𝑥 = 𝑧 → 𝑦 = 𝑧 )
19	18	19.35i	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 𝑦 = 𝑧 )
20	11 16 19	3jaoi	⊢ ( ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) → ∃ 𝑥 𝑦 = 𝑧 )
21	10 20	impbii	⊢ ( ∃ 𝑥 𝑦 = 𝑧 ↔ ( 𝑦 = 𝑧 ∨ ∀ 𝑥 𝑥 = 𝑦 ∨ ∀ 𝑥 𝑥 = 𝑧 ) )