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

Theorem reu4 3387
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 3153 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
2 rmo4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32rmo4 3386 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 729 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 264 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wral 2912  wrex 2913  ∃!wreu 2914  ∃*wrmo 2915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-cleq 2619  df-clel 2622  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920
This theorem is referenced by:  reuind  3398  oawordeulem  7580  fin23lem23  9093  nqereu  9696  receu  10617  lbreu  10918  cju  10961  fprodser  14599  divalglem9  15043  ndvdssub  15052  qredeu  15291  pj1eu  18025  efgredeu  18081  lspsneu  19037  qtopeu  21424  qtophmeo  21525  minveclem7  23109  ig1peu  23830  coeeu  23880  plydivalg  23953  hlcgreu  25408  mirreu3  25444  trgcopyeu  25593  axcontlem2  25740  umgr2edg1  25990  umgr2edgneu  25993  usgredgreu  25997  uspgredg2vtxeu  25999  4cycl2vnunb  27012  frgr2wwlk1  27046  frgr2wwlkeqm  27048  minvecolem7  27579  hlimreui  27936  riesz4i  28762  cdjreui  29131  xreceu  29407  cvmseu  30958  nocvxmin  31546  segconeu  31752  outsideofeu  31872  poimirlem4  33031  bfp  33241  exidu1  33273  rngoideu  33320  lshpsmreu  33862  cdleme  35314  lcfl7N  36256  mapdpg  36461  hdmap14lem6  36631  mpaaeu  37187  icceuelpart  40658
  Copyright terms: Public domain W3C validator