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

Theorem eu5 2336
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  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )

Proof of Theorem eu5
StepHypRef Expression
1 abai 809 . 2  |-  ( ( E. x ph  /\  E! x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
2 euex 2334 . . 3  |-  ( E! x ph  ->  E. x ph )
32pm4.71ri 643 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E! x ph ) )
4 df-mo 2315 . . 3  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
54anbi2i 705 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
61, 3, 53bitr4i 285 1  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   E.wex 1674   E!weu 2310   E*wmo 2311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-eu 2314  df-mo 2315
This theorem is referenced by:  exmoeu2  2337  eu3v  2338  eumo  2339  eu2  2349  eu4  2358  euim  2363  2euex  2384  2euswap  2388  2exeu  2389  2eu4  2396  reu5  3020  reuss2  3735  n0moeu  3757  reusv2lem1  4618  funcnv3  5666  fnres  5714  mptfnf  5721  fnopabg  5723  brprcneu  5881  dff3  6058  finnisoeu  8570  dfac2  8587  recmulnq  9415  uptx  20689  hausflf2  21062  adjeu  27591  bnj151  29737  bnj600  29779  bj-eu3f  31487  fzisoeu  37556  ellimciota  37732
  Copyright terms: Public domain W3C validator