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

Theorem reu4 3367
 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 3136 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
2 rmo4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32rmo4 3366 . . 3 (∃*𝑥𝐴 𝜑 ↔ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 726 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑) ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 263 1 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∀𝑥𝐴𝑦𝐴 ((𝜑𝜓) → 𝑥 = 𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-cleq 2603  df-clel 2606  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904 This theorem is referenced by:  reuind  3378  oawordeulem  7521  fin23lem23  9031  nqereu  9630  receu  10551  lbreu  10852  cju  10893  fprodser  14518  divalglem9  14962  ndvdssub  14971  qredeu  15210  pj1eu  17932  efgredeu  17988  lspsneu  18944  qtopeu  21329  qtophmeo  21430  minveclem7  23014  ig1peu  23735  coeeu  23785  plydivalg  23858  hlcgreu  25313  mirreu3  25349  trgcopyeu  25498  axcontlem2  25645  usgra2edg1  25912  usgraedgreu  25917  nbgraf1olem1  25970  4cycl2vnunb  26544  frg2wot1  26584  minvecolem7  27123  hlimreui  27480  riesz4i  28306  cdjreui  28675  xreceu  28961  cvmseu  30512  nocvxmin  31090  segconeu  31288  outsideofeu  31408  poimirlem4  32583  bfp  32793  exidu1  32825  rngoideu  32872  lshpsmreu  33414  cdleme  34866  lcfl7N  35808  mapdpg  36013  hdmap14lem6  36183  mpaaeu  36739  icceuelpart  39974  umgr2edg1  40438  umgr2edgneu  40441  usgredgreu  40445  uspgredg2vtxeu  40447  4cycl2vnunb-av  41460  frgr2wwlk1  41494  frgr2wwlkeqm  41496
 Copyright terms: Public domain W3C validator