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

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

Proof of Theorem euex
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 ax-17 1396 . . 3 (φyφ)
21eu1 1903 . 2 (∃!xφx(φ y([y / x]φx = y)))
3 exsimpl 1486 . 2 (x(φ y([y / x]φx = y)) → xφ)
42, 3sylbi 114 1 (∃!xφxφ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wal 1224  wex 1358  [wsb 1623  ∃!weu 1878
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 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406
This theorem depends on definitions:  df-bi 110  df-nf 1326  df-sb 1624  df-eu 1881
This theorem is referenced by:  eu2  1922  eu3h  1923  eu5  1925  exmoeudc  1941  eupickbi  1960  2eu2ex  1967  euxfrdc  2700  repizf  3843  eusvnf  4131  eusvnfb  4132  tz6.12c  5124  ndmfvg  5125  nfvres  5127  0fv  5129  eusvobj2  5418  fnoprabg  5521
  Copyright terms: Public domain W3C validator