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

Theorem reu4 3708
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 3413 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
2 rmo4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32rmo4 3707 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 625 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 278 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wral 3133  wrex 3134  ∃!wreu 3135  ∃*wrmo 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2624  df-eu 2655  df-clel 2896  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141
This theorem is referenced by:  reuind  3730  oawordeulem  8176  fin23lem23  9746  nqereu  10349  receu  11283  lbreu  11587  cju  11630  fprodser  15303  divalglem9  15750  ndvdssub  15758  qredeu  16000  pj1eu  18822  efgredeu  18878  lspsneu  19895  qtopeu  22324  qtophmeo  22425  minveclem7  24042  ig1peu  24775  coeeu  24825  plydivalg  24898  hlcgreu  26415  mirreu3  26451  trgcopyeu  26603  axcontlem2  26762  umgr2edg1  27004  umgr2edgneu  27007  usgredgreu  27011  uspgredg2vtxeu  27013  4cycl2vnunb  28078  frgr2wwlk1  28117  minvecolem7  28669  hlimreui  29025  riesz4i  29849  cdjreui  30218  xreceu  30609  cvmseu  32580  nocvxmin  33305  segconeu  33529  outsideofeu  33649  poimirlem4  35006  bfp  35207  exidu1  35239  rngoideu  35286  lshpsmreu  36350  cdleme  37801  lcfl7N  38742  mapdpg  38947  hdmap14lem6  39114  mpaaeu  40010  icceuelpart  43879
  Copyright terms: Public domain W3C validator