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

Theorem eu5 2311
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 795 . 2  |-  ( ( E. x ph  /\  E! x ph )  <->  ( E. x ph  /\  ( E. x ph  ->  E! x ph ) ) )
2 euex 2309 . . 3  |-  ( E! x ph  ->  E. x ph )
32pm4.71ri 633 . 2  |-  ( E! x ph  <->  ( E. x ph  /\  E! x ph ) )
4 df-mo 2288 . . 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 1613   E!weu 2283   E*wmo 2284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1614  df-eu 2287  df-mo 2288
This theorem is referenced by:  exmoeu2  2312  eu3v  2313  eumo  2314  eu2  2327  eu4  2339  euim  2344  2euex  2366  2euswap  2370  2exeu  2371  2eu1OLD  2377  2eu4  2380  reu5  3073  reuss2  3785  n0moeu  3807  reusv2lem1  4657  funcnv3  5655  fnres  5703  fnopabg  5710  brprcneu  5865  dff3  6045  finnisoeu  8511  dfac2  8528  recmulnq  9359  uptx  20252  hausflf2  20625  adjeu  26935  mptfnf  27648  fzisoeu  31703  ellimciota  31823  bnj151  34078  bnj600  34120  bj-eu3f  34556
  Copyright terms: Public domain W3C validator