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

Theorem eu5 2292
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 802 . 2  |-  ( ( E. x ph  /\  E! x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
2 euex 2290 . . 3  |-  ( E! x ph  ->  E. x ph )
32pm4.71ri 637 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E! x ph ) )
4 df-mo 2270 . . 3  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
54anbi2i 698 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
61, 3, 53bitr4i 280 1  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   E.wex 1659   E!weu 2265   E*wmo 2266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-eu 2269  df-mo 2270
This theorem is referenced by:  exmoeu2  2293  eu3v  2294  eumo  2295  eu2  2305  eu4  2314  euim  2319  2euex  2340  2euswap  2344  2exeu  2345  2eu1OLD  2351  2eu4  2354  reu5  3044  reuss2  3753  n0moeu  3775  reusv2lem1  4621  funcnv3  5658  fnres  5706  mptfnf  5713  fnopabg  5715  brprcneu  5870  dff3  6046  finnisoeu  8544  dfac2  8561  recmulnq  9389  uptx  20626  hausflf2  20999  adjeu  27527  bnj151  29683  bnj600  29725  bj-eu3f  31399  fzisoeu  37359  ellimciota  37513
  Copyright terms: Public domain W3C validator