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

Theorem eu5 1989
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 1972 . . 3 (∃!𝑥𝜑 → ∃𝑥𝜑)
2 eumo 1974 . . 3 (∃!𝑥𝜑 → ∃*𝑥𝜑)
31, 2jca 300 . 2 (∃!𝑥𝜑 → (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
4 df-mo 1946 . . . . 5 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
54biimpi 118 . . . 4 (∃*𝑥𝜑 → (∃𝑥𝜑 → ∃!𝑥𝜑))
65imp 122 . . 3 ((∃*𝑥𝜑 ∧ ∃𝑥𝜑) → ∃!𝑥𝜑)
76ancoms 264 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) → ∃!𝑥𝜑)
83, 7impbii 124 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wex 1422  ∃!weu 1942  ∃*wmo 1943
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-eu 1945  df-mo 1946
This theorem is referenced by:  exmoeu2  1990  euan  1998  eu4  2004  euim  2010  euexex  2027  2euex  2029  2euswapdc  2033  2exeu  2034  reu5  2567  reuss2  3251  funcnv3  4992  fnres  5046  fnopabg  5053  brprcneu  5202  dff3im  5344  recmulnqg  6643
  Copyright terms: Public domain W3C validator