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 ⊢∃y∀xφ↔x=y↔∃y∀xx=y→φ∧∃z∀xφ→x=z

Proof

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