MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eumo Structured version   Visualization version   GIF version

Theorem eumo 2497
Description: Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
Assertion
Ref Expression
eumo (∃!𝑥𝜑 → ∃*𝑥𝜑)

Proof of Theorem eumo
StepHypRef Expression
1 eu5 2494 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
21simprbi 480 1 (∃!𝑥𝜑 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1702  ∃!weu 2468  ∃*wmo 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-eu 2472  df-mo 2473
This theorem is referenced by:  eumoi  2498  euimmo  2520  moaneu  2531  eupick  2534  2eumo  2543  2exeu  2547  2eu2  2552  2eu5  2555  moeq3  3377  euabex  4920  nfunsn  6212  dff3  6358  fnoprabg  6746  zfrep6  7119  nqerf  9737  f1otrspeq  17848  uptx  21409  txcn  21410  pm14.12  38442
  Copyright terms: Public domain W3C validator