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

Theorem reu4 3552
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 3308 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
2 rmo4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32rmo4 3551 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 609 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 264 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  wral 3061  wrex 3062  ∃!wreu 3063  ∃*wrmo 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clel 2767  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069
This theorem is referenced by:  reuind  3563  oawordeulem  7792  fin23lem23  9354  nqereu  9957  receu  10878  lbreu  11179  cju  11222  fprodser  14886  divalglem9  15332  ndvdssub  15341  qredeu  15579  pj1eu  18316  efgredeu  18372  lspsneu  19336  qtopeu  21740  qtophmeo  21841  minveclem7  23425  ig1peu  24151  coeeu  24201  plydivalg  24274  hlcgreu  25734  mirreu3  25770  trgcopyeu  25919  axcontlem2  26066  umgr2edg1  26325  umgr2edgneu  26328  usgredgreu  26332  uspgredg2vtxeu  26334  4cycl2vnunb  27472  frgr2wwlk1  27511  minvecolem7  28079  hlimreui  28436  riesz4i  29262  cdjreui  29631  xreceu  29970  cvmseu  31596  nocvxmin  32231  segconeu  32455  outsideofeu  32575  poimirlem4  33746  bfp  33955  exidu1  33987  rngoideu  34034  lshpsmreu  34918  cdleme  36370  lcfl7N  37311  mapdpg  37516  hdmap14lem6  37683  mpaaeu  38246  icceuelpart  41897
  Copyright terms: Public domain W3C validator