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

Theorem reu4 3433
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 3189 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
2 rmo4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32rmo4 3432 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 730 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 264 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wral 2941  wrex 2942  ∃!wreu 2943  ∃*wrmo 2944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-cleq 2644  df-clel 2647  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949
This theorem is referenced by:  reuind  3444  oawordeulem  7679  fin23lem23  9186  nqereu  9789  receu  10710  lbreu  11011  cju  11054  fprodser  14723  divalglem9  15171  ndvdssub  15180  qredeu  15419  pj1eu  18155  efgredeu  18211  lspsneu  19171  qtopeu  21567  qtophmeo  21668  minveclem7  23252  ig1peu  23976  coeeu  24026  plydivalg  24099  hlcgreu  25558  mirreu3  25594  trgcopyeu  25743  axcontlem2  25890  umgr2edg1  26148  umgr2edgneu  26151  usgredgreu  26155  uspgredg2vtxeu  26157  4cycl2vnunb  27270  frgr2wwlk1  27309  minvecolem7  27867  hlimreui  28224  riesz4i  29050  cdjreui  29419  xreceu  29758  cvmseu  31384  nocvxmin  32019  segconeu  32243  outsideofeu  32363  poimirlem4  33543  bfp  33753  exidu1  33785  rngoideu  33832  lshpsmreu  34714  cdleme  36165  lcfl7N  37107  mapdpg  37312  hdmap14lem6  37482  mpaaeu  38037  icceuelpart  41697
  Copyright terms: Public domain W3C validator