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

Theorem eu5 2047
 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 2030 . . 3 (∃!𝑥𝜑 → ∃𝑥𝜑)
2 eumo 2032 . . 3 (∃!𝑥𝜑 → ∃*𝑥𝜑)
31, 2jca 304 . 2 (∃!𝑥𝜑 → (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
4 df-mo 2004 . . . . 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 1469  ∃!weu 2000  ∃*wmo 2001 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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004 This theorem is referenced by:  exmoeu2  2048  euan  2056  eu4  2062  euim  2068  euexex  2085  2euex  2087  2euswapdc  2091  2exeu  2092  reu5  2646  reuss2  3360  funcnv3  5192  fnres  5246  fnopabg  5253  brprcneu  5421  dff3im  5572  recmulnqg  7222  uptx  12480
 Copyright terms: Public domain W3C validator