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

Theorem eu5 2066
Description: Uniqueness in terms of "at most one". (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
Assertion
Ref Expression
eu5 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))

Proof of Theorem eu5
StepHypRef Expression
1 euex 2049 . . 3 (∃!𝑥𝜑 → ∃𝑥𝜑)
2 eumo 2051 . . 3 (∃!𝑥𝜑 → ∃*𝑥𝜑)
31, 2jca 304 . 2 (∃!𝑥𝜑 → (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
4 df-mo 2023 . . . . 5 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
54biimpi 119 . . . 4 (∃*𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑))
65imp 123 . . 3 ((∃*𝑥𝜑 ∧ ∃𝑥𝜑) → ∃!𝑥𝜑)
76ancoms 266 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) → ∃!𝑥𝜑)
83, 7impbii 125 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wex 1485  ∃!weu 2019  ∃*wmo 2020
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023
This theorem is referenced by:  exmoeu2  2067  euan  2075  eu4  2081  euim  2087  euexex  2104  2euex  2106  2euswapdc  2110  2exeu  2111  reu5  2682  reuss2  3407  funcnv3  5260  fnres  5314  fnopabg  5321  brprcneu  5489  dff3im  5641  recmulnqg  7353  uptx  13068
  Copyright terms: Public domain W3C validator