MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reu4 Structured version   Visualization version   GIF version

Theorem reu4 3725
Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994.)
Hypothesis
Ref Expression
rmo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
reu4 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu4
StepHypRef Expression
1 reu5 3367 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
2 rmo4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32rmo4 3724 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 621 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 274 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wral 3051  wrex 3060  ∃!wreu 3363  ∃*wrmo 3364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-mo 2529  df-eu 2558  df-clel 2803  df-ral 3052  df-rex 3061  df-rmo 3365  df-reu 3366
This theorem is referenced by:  reuind  3747  oawordeulem  8574  fin23lem23  10358  nqereu  10961  receu  11898  lbreu  12208  cju  12252  fprodser  15944  divalglem9  16396  ndvdssub  16404  qredeu  16652  pj1eu  19688  efgredeu  19744  lspsneu  21098  qtopeu  23706  qtophmeo  23807  minveclem7  25449  ig1peu  26197  coeeu  26247  plydivalg  26322  nocvxmin  27803  hlcgreu  28540  mirreu3  28576  trgcopyeu  28728  axcontlem2  28894  umgr2edg1  29142  umgr2edgneu  29145  usgredgreu  29149  uspgredg2vtxeu  29151  4cycl2vnunb  30218  frgr2wwlk1  30257  minvecolem7  30811  hlimreui  31167  riesz4i  31991  cdjreui  32360  xreceu  32784  cvmseu  35115  segconeu  35846  outsideofeu  35966  poimirlem4  37336  bfp  37536  exidu1  37568  rngoideu  37615  lshpsmreu  38818  cdleme  40270  lcfl7N  41211  mapdpg  41416  hdmap14lem6  41583  mpaaeu  42846  icceuelpart  47042  isuspgrim0lem  47484
  Copyright terms: Public domain W3C validator