Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mopick GIF version

Theorem mopick 1978
 Description: "At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.)
Assertion
Ref Expression
mopick ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))

Proof of Theorem mopick
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ax-17 1419 . . . 4 ((𝜑𝜓) → ∀𝑦(𝜑𝜓))
2 hbs1 1814 . . . . 5 ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
3 hbs1 1814 . . . . 5 ([𝑦 / 𝑥]𝜓 → ∀𝑥[𝑦 / 𝑥]𝜓)
42, 3hban 1439 . . . 4 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → ∀𝑥([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
5 sbequ12 1654 . . . . 5 (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
6 sbequ12 1654 . . . . 5 (𝑥 = 𝑦 → (𝜓 ↔ [𝑦 / 𝑥]𝜓))
75, 6anbi12d 442 . . . 4 (𝑥 = 𝑦 → ((𝜑𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)))
81, 4, 7cbvexh 1638 . . 3 (∃𝑥(𝜑𝜓) ↔ ∃𝑦([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
9 ax-17 1419 . . . . . . 7 (𝜑 → ∀𝑦𝜑)
109mo3h 1953 . . . . . 6 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
11 ax-4 1400 . . . . . . 7 (∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1211sps 1430 . . . . . 6 (∀𝑥𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
1310, 12sylbi 114 . . . . 5 (∃*𝑥𝜑 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
14 sbequ2 1652 . . . . . . . . 9 (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜓𝜓))
1514imim2i 12 . . . . . . . 8 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → ([𝑦 / 𝑥]𝜓𝜓)))
1615expd 245 . . . . . . 7 (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑 → ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓𝜓))))
1716com4t 79 . . . . . 6 ([𝑦 / 𝑥]𝜑 → ([𝑦 / 𝑥]𝜓 → (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑𝜓))))
1817imp 115 . . . . 5 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → (((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → (𝜑𝜓)))
1913, 18syl5 28 . . . 4 (([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → (∃*𝑥𝜑 → (𝜑𝜓)))
2019exlimiv 1489 . . 3 (∃𝑦([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓) → (∃*𝑥𝜑 → (𝜑𝜓)))
218, 20sylbi 114 . 2 (∃𝑥(𝜑𝜓) → (∃*𝑥𝜑 → (𝜑𝜓)))
2221impcom 116 1 ((∃*𝑥𝜑 ∧ ∃𝑥(𝜑𝜓)) → (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1241  ∃wex 1381  [wsb 1645  ∃*wmo 1901 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904 This theorem is referenced by:  eupick  1979  mopick2  1983  moexexdc  1984  euexex  1985  morex  2725  imadif  4979  funimaexglem  4982
 Copyright terms: Public domain W3C validator