Metamath Proof Explorer

Theorem eu6lem

Description: Lemma of eu6im . A dissection of an idiom characterizing existential uniqueness. (Contributed by NM, 12-Aug-1993) This used to be the definition of the unique existential quantifier, while df-eu was then proved as dfeu . (Revised by BJ, 30-Sep-2022) (Proof shortened by Wolf Lammen, 3-Jan-2023) Extract common proof lines. (Revised by Wolf Lammen, 3-Mar-2023)

Ref Expression
Assertion eu6lem ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 19.42v ⊢ ( ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝑦 = 𝑧 ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∃ 𝑧 𝑦 = 𝑧 ) )
2 alsyl ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) )
3 equvelv ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 = 𝑧 ) ↔ 𝑦 = 𝑧 )
4 2 3 sylib ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) → 𝑦 = 𝑧 )
5 4 pm4.71i ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ↔ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ∧ 𝑦 = 𝑧 ) )
6 albiim ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ∧ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
7 6 biancomi ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) )
8 equequ2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) )
9 8 imbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝜑 → 𝑥 = 𝑦 ) ↔ ( 𝜑 → 𝑥 = 𝑧 ) ) )
10 9 albidv ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
11 10 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ) )
12 7 11 syl5bb ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ) )
13 12 pm5.32ri ⊢ ( ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝑦 = 𝑧 ) ↔ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ∧ 𝑦 = 𝑧 ) )
14 5 13 bitr4i ⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝑦 = 𝑧 ) )
15 14 exbii ⊢ ( ∃ 𝑧 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ 𝑦 = 𝑧 ) )
16 ax6evr ⊢ ∃ 𝑧 𝑦 = 𝑧
17 16 biantru ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ∧ ∃ 𝑧 𝑦 = 𝑧 ) )
18 1 15 17 3bitr4ri ⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑧 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
19 18 exbii ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ∃ 𝑦 ∃ 𝑧 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
20 exdistrv ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) ↔ ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )
21 19 20 bitri ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) ↔ ( ∃ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) )