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

Theorem euex 1946
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 1435 . . 3 (𝜑 → ∀𝑦𝜑)
21eu1 1941 . 2 (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
3 exsimpl 1524 . 2 (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑𝑥 = 𝑦)) → ∃𝑥𝜑)
42, 3sylbi 118 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wal 1257  wex 1397  [wsb 1661  ∃!weu 1916
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-eu 1919
This theorem is referenced by:  eu2  1960  eu3h  1961  eu5  1963  exmoeudc  1979  eupickbi  1998  2eu2ex  2005  euxfrdc  2750  repizf  3901  eusvnf  4213  eusvnfb  4214  tz6.12c  5231  ndmfvg  5232  nfvres  5234  0fv  5236  eusvobj2  5526  fnoprabg  5630
  Copyright terms: Public domain W3C validator