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

Theorem eu5 2290
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 793 . 2  |-  ( ( E. x ph  /\  E! x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
2 euex 2288 . . 3  |-  ( E! x ph  ->  E. x ph )
32pm4.71ri 633 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E! x ph ) )
4 df-mo 2265 . . 3  |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
54anbi2i 694 . 2  |-  ( ( E. x ph  /\  E* x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
61, 3, 53bitr4i 277 1  |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   E.wex 1587   E!weu 2260   E*wmo 2261
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-eu 2264  df-mo 2265
This theorem is referenced by:  exmoeu2  2291  eu3v  2292  eumo  2293  eu2  2309  eu4  2325  euim  2331  euanOLD  2339  2euex  2360  2euswap  2364  2exeu  2365  2eu1OLD  2372  2eu4  2375  reu5  3029  reuss2  3725  n0moeu  3745  reusv2lem1  4588  funcnv3  5574  fnres  5622  fnopabg  5629  brprcneu  5779  dff3  5952  finnisoeu  8381  dfac2  8398  recmulnq  9231  uptx  19311  hausflf2  19684  adjeu  25425  mptfnf  26107  bnj151  32167  bnj600  32209  bj-eu3f  32645
  Copyright terms: Public domain W3C validator