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

Theorem euex 1930
 Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
euex (∃!𝑥𝜑 → ∃𝑥𝜑)

Proof of Theorem euex
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ax-17 1419 . . 3 (𝜑 → ∀𝑦𝜑)
21eu1 1925 . 2 (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
3 exsimpl 1508 . 2 (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑𝑥 = 𝑦)) → ∃𝑥𝜑)
42, 3sylbi 114 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97  ∀wal 1241  ∃wex 1381  [wsb 1645  ∃!weu 1900 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 This theorem is referenced by:  eu2  1944  eu3h  1945  eu5  1947  exmoeudc  1963  eupickbi  1982  2eu2ex  1989  euxfrdc  2727  repizf  3873  eusvnf  4185  eusvnfb  4186  tz6.12c  5203  ndmfvg  5204  nfvres  5206  0fv  5208  eusvobj2  5498  fnoprabg  5602
 Copyright terms: Public domain W3C validator