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

Theorem eu5 2495
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 835 . 2 ((∃𝑥𝜑 ∧ ∃!𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
2 euex 2493 . . 3 (∃!𝑥𝜑 → ∃𝑥𝜑)
32pm4.71ri 664 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃!𝑥𝜑))
4 df-mo 2474 . . 3 (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
54anbi2i 729 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃!𝑥𝜑)))
61, 3, 53bitr4i 292 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wex 1701  ∃!weu 2469  ∃*wmo 2470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-eu 2473  df-mo 2474
This theorem is referenced by:  exmoeu2  2496  eu3v  2497  eumo  2498  eu2  2508  eu4  2517  euim  2522  2euex  2543  2euswap  2547  2exeu  2548  2eu4  2555  reu5  3151  reuss2  3888  n0moeu  3918  reusv2lem1  4833  funcnv3  5922  fnres  5970  mptfnf  5977  fnopabg  5979  brprcneu  6146  dff3  6333  finnisoeu  8888  dfac2  8905  recmulnq  9738  uptx  21351  hausflf2  21725  adjeu  28618  bnj151  30690  bnj600  30732  nosino  31610  nosifv  31611  bj-eu3f  32507  fzisoeu  39009  ellimciota  39278
  Copyright terms: Public domain W3C validator