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

Theorem eu5 2305
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 2303 . . 3  |-  ( E! x ph  ->  E. x ph )
32pm4.71ri 633 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E! x ph ) )
4 df-mo 2280 . . 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 1596   E!weu 2275   E*wmo 2276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-eu 2279  df-mo 2280
This theorem is referenced by:  exmoeu2  2306  eu3v  2307  eumo  2308  eu2  2324  eu4  2340  euim  2346  euanOLD  2354  2euex  2375  2euswap  2379  2exeu  2380  2eu1OLD  2387  2eu4  2390  reu5  3077  reuss2  3778  n0moeu  3798  reusv2lem1  4648  funcnv3  5647  fnres  5695  fnopabg  5702  brprcneu  5857  dff3  6032  finnisoeu  8490  dfac2  8507  recmulnq  9338  uptx  19858  hausflf2  20231  adjeu  26481  mptfnf  27168  fzisoeu  31077  ellimciota  31156  bnj151  33014  bnj600  33056  bj-eu3f  33494
  Copyright terms: Public domain W3C validator