This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 19.42v ⊢ ∃ z ∀ x φ ↔ x = y ∧ y = z ↔ ∀ x φ ↔ x = y ∧ ∃ z y = z
2 alsyl ⊢ ∀ x x = y → φ ∧ ∀ x φ → x = z → ∀ x x = y → x = z
3 equvelv ⊢ ∀ x x = y → x = z ↔ y = z
4 2 3 sylib ⊢ ∀ x x = y → φ ∧ ∀ x φ → x = z → y = z
5 4 pm4.71i ⊢ ∀ x x = y → φ ∧ ∀ x φ → x = z ↔ ∀ x x = y → φ ∧ ∀ x φ → x = z ∧ y = z
6 albiim ⊢ ∀ x φ ↔ x = y ↔ ∀ x φ → x = y ∧ ∀ x x = y → φ
7 6 biancomi ⊢ ∀ x φ ↔ x = y ↔ ∀ x x = 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 → ∀ x x = y → φ ∧ ∀ x φ → x = y ↔ ∀ x x = y → φ ∧ ∀ x φ → x = z
12 7 11 bitrid ⊢ y = z → ∀ x φ ↔ x = y ↔ ∀ x x = y → φ ∧ ∀ x φ → x = z
13 12 pm5.32ri ⊢ ∀ x φ ↔ x = y ∧ y = z ↔ ∀ x x = y → φ ∧ ∀ x φ → x = z ∧ y = z
14 5 13 bitr4i ⊢ ∀ x x = y → φ ∧ ∀ x φ → x = z ↔ ∀ x φ ↔ x = y ∧ y = z
15 14 exbii ⊢ ∃ z ∀ x x = y → φ ∧ ∀ x φ → x = z ↔ ∃ z ∀ x φ ↔ x = y ∧ y = z
16 ax6evr ⊢ ∃ z y = z
17 16 biantru ⊢ ∀ x φ ↔ x = y ↔ ∀ x φ ↔ x = y ∧ ∃ z y = z
18 1 15 17 3bitr4ri ⊢ ∀ x φ ↔ x = y ↔ ∃ z ∀ x x = y → φ ∧ ∀ x φ → x = z
19 18 exbii ⊢ ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∃ z ∀ x x = y → φ ∧ ∀ x φ → x = z
20 exdistrv ⊢ ∃ y ∃ z ∀ x x = y → φ ∧ ∀ x φ → x = z ↔ ∃ y ∀ x x = y → φ ∧ ∃ z ∀ x φ → x = z
21 19 20 bitri ⊢ ∃ y ∀ x φ ↔ x = y ↔ ∃ y ∀ x x = y → φ ∧ ∃ z ∀ x φ → x = z