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

Metamath Proof Explorer

Theorem mo3

Description: Alternate definition of the at-most-one quantifier. Definition of BellMachover p. 460, except that definition has the side condition that y not occur in ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995) (Proof shortened by Wolf Lammen, 18-Aug-2019) Remove dependency on ax-13 . (Revised by BJ and WL, 29-Jan-2023)

Ref Expression
Hypothesis mo3.nf ⊢ Ⅎ y φ
Assertion mo3 ⊢ ∃* x φ ↔ ∀ x ∀ y φ ∧ y x φ → x = y

Proof

Step Hyp Ref Expression
1 mo3.nf ⊢ Ⅎ y φ
2 nfmo1 ⊢ Ⅎ x ∃* x φ
3 1 nfmov ⊢ Ⅎ y ∃* x φ
4 df-mo ⊢ ∃* x φ ↔ ∃ z ∀ x φ → x = z
5 sp ⊢ ∀ x φ → x = z → φ → x = z
6 spsbim ⊢ ∀ x φ → x = z → y x φ → y x x = z
7 equsb3 ⊢ y x x = z ↔ y = z
8 6 7 imbitrdi ⊢ ∀ x φ → x = z → y x φ → y = z
9 5 8 anim12d ⊢ ∀ x φ → x = z → φ ∧ y x φ → x = z ∧ y = z
10 equtr2 ⊢ x = z ∧ y = z → x = y
11 9 10 syl6 ⊢ ∀ x φ → x = z → φ ∧ y x φ → x = y
12 11 exlimiv ⊢ ∃ z ∀ x φ → x = z → φ ∧ y x φ → x = y
13 4 12 sylbi ⊢ ∃* x φ → φ ∧ y x φ → x = y
14 3 13 alrimi ⊢ ∃* x φ → ∀ y φ ∧ y x φ → x = y
15 2 14 alrimi ⊢ ∃* x φ → ∀ x ∀ y φ ∧ y x φ → x = y
16 nfs1v ⊢ Ⅎ x y x φ
17 pm3.21 ⊢ y x φ → φ → φ ∧ y x φ
18 17 imim1d ⊢ y x φ → φ ∧ y x φ → x = y → φ → x = y
19 16 18 alimd ⊢ y x φ → ∀ x φ ∧ y x φ → x = y → ∀ x φ → x = y
20 19 com12 ⊢ ∀ x φ ∧ y x φ → x = y → y x φ → ∀ x φ → x = y
21 20 aleximi ⊢ ∀ y ∀ x φ ∧ y x φ → x = y → ∃ y y x φ → ∃ y ∀ x φ → x = y
22 1 sb8ef ⊢ ∃ x φ ↔ ∃ y y x φ
23 1 mof ⊢ ∃* x φ ↔ ∃ y ∀ x φ → x = y
24 21 22 23 3imtr4g ⊢ ∀ y ∀ x φ ∧ y x φ → x = y → ∃ x φ → ∃* x φ
25 moabs ⊢ ∃* x φ ↔ ∃ x φ → ∃* x φ
26 24 25 sylibr ⊢ ∀ y ∀ x φ ∧ y x φ → x = y → ∃* x φ
27 26 alcoms ⊢ ∀ x ∀ y φ ∧ y x φ → x = y → ∃* x φ
28 15 27 impbii ⊢ ∃* x φ ↔ ∀ x ∀ y φ ∧ y x φ → x = y