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

Theorem euex 1975
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 1462 . . 3 (𝜑 → ∀𝑦𝜑)
21eu1 1970 . 2 (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑𝑥 = 𝑦)))
3 exsimpl 1551 . 2 (∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑𝑥 = 𝑦)) → ∃𝑥𝜑)
42, 3sylbi 119 1 (∃!𝑥𝜑 → ∃𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wal 1285  wex 1424  [wsb 1689  ∃!weu 1945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-eu 1948
This theorem is referenced by:  eu2  1989  eu3h  1990  eu5  1992  exmoeudc  2008  eupickbi  2027  2eu2ex  2034  euxfrdc  2792  repizf  3929  eusvnf  4248  eusvnfb  4249  tz6.12c  5291  ndmfvg  5292  nfvres  5294  0fv  5296  eusvobj2  5593  fnoprabg  5697
  Copyright terms: Public domain W3C validator