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

Theorem euex 2309
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2329. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)
Assertion
Ref Expression
euex  |-  ( E! x ph  ->  E. x ph )

Proof of Theorem euex
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-eu 2287 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 ax6ev 1750 . . . . 5  |-  E. x  x  =  y
3 bi2 198 . . . . . 6  |-  ( (
ph 
<->  x  =  y )  ->  ( x  =  y  ->  ph ) )
43com12 31 . . . . 5  |-  ( x  =  y  ->  (
( ph  <->  x  =  y
)  ->  ph ) )
52, 4eximii 1659 . . . 4  |-  E. x
( ( ph  <->  x  =  y )  ->  ph )
6519.35i 1690 . . 3  |-  ( A. x ( ph  <->  x  =  y )  ->  E. x ph )
76exlimiv 1723 . 2  |-  ( E. y A. x (
ph 
<->  x  =  y )  ->  E. x ph )
81, 7sylbi 195 1  |-  ( E! x ph  ->  E. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1393   E.wex 1613   E!weu 2283
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-ex 1614  df-eu 2287
This theorem is referenced by:  eu5  2311  exmoeu  2317  euan  2351  eupickbi  2361  2eu2ex  2368  2exeu  2371  euxfr  3285  eusvnf  4651  eusvnfb  4652  reusv2lem2  4658  reusv2lem3  4659  csbiota  5586  dffv3  5868  tz6.12c  5891  ndmfv  5896  dff3  6045  csbriota  6270  eusvobj2  6289  fnoprabg  6402  zfrep6  6767  dfac5lem5  8525  initoeu1  15417  initoeu1w  15418  initoeu2  15422  termoeu1  15424  termoeu1w  15425  grpidval  16014  0g0  16017  txcn  20253  unnf  30077  unqsym1  30095  moxfr  30829  eu2ndop1stv  32410  afveu  32441  zrninitoringc  33023  bnj605  34108  bnj607  34117  bnj906  34131  bnj908  34132
  Copyright terms: Public domain W3C validator