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

Theorem euex 2308
Description: Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2328. (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

Proof of Theorem euex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-eu 2286 . 2
2 ax6ev 1749 . . . . 5
3 bi2 198 . . . . . 6
43com12 31 . . . . 5
52, 4eximii 1658 . . . 4
6519.35i 1689 . . 3
76exlimiv 1722 . 2
81, 7sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  E.wex 1612  E!weu 2282
This theorem is referenced by:  eu5  2310  exmoeu  2316  euan  2351  eupickbi  2361  2eu2ex  2368  2exeu  2371  euxfr  3285  eusvnf  4647  eusvnfb  4648  reusv2lem2  4654  reusv2lem3  4655  csbiota  5585  dffv3  5867  tz6.12c  5890  ndmfv  5895  dff3  6044  csbriota  6269  eusvobj2  6289  fnoprabg  6403  zfrep6  6768  dfac5lem5  8529  grpidval  15887  0g0  15890  txcn  20127  unnf  29872  unqsym1  29890  moxfr  30624  eu2ndop1stv  32207  afveu  32238  initoeu1  32617  initoeu1w  32618  initoeu2  32622  termoeu1  32624  termoeu1w  32625  zrninitoringc  32879  bnj605  33965  bnj607  33974  bnj906  33988  bnj908  33989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-eu 2286
  Copyright terms: Public domain W3C validator