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

Theorem eu5 2524
Description: Uniqueness in terms of "at most one." Revised to reduce dependencies on axioms. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.)
Assertion
Ref Expression
eu5 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Proof of Theorem eu5
StepHypRef Expression
1 abai 853 . 2 ((∃𝑥𝜑 ∧ ∃!𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
2 euex 2522 . . 3 (∃!𝑥𝜑 → ∃𝑥𝜑)
32pm4.71ri 666 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃!𝑥𝜑))
4 df-mo 2503 . . 3 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
54anbi2i 730 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
61, 3, 53bitr4i 292 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wex 1744  ∃!weu 2498  ∃*wmo 2499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-eu 2502  df-mo 2503
This theorem is referenced by:  exmoeu2  2525  eu3v  2526  eumoOLD  2528  eu2  2538  eu4  2547  euim  2552  2euex  2573  2euswap  2577  2exeu  2578  2eu4  2585  reu5  3189  reuss2  3940  n0moeu  3970  reusv2lem1  4898  funcnv3  5997  fnres  6045  mptfnf  6053  fnopabg  6055  brprcneu  6222  dff3  6412  finnisoeu  8974  dfac2  8991  recmulnq  9824  uptx  21476  hausflf2  21849  adjeu  28876  bnj151  31073  bnj600  31115  nosupno  31974  nosupfv  31977  bj-eu3f  32954  fzisoeu  39828  ellimciota  40164
  Copyright terms: Public domain W3C validator