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

Theorem reubidv 3398
Description: Formula-building rule for restricted existential uniqueness quantifier (deduction form). (Contributed by NM, 17-Oct-1996.)
Hypothesis
Ref Expression
rmobidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
reubidv (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidv
StepHypRef Expression
1 rmobidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 480 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3396 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wcel 2108  ∃!wreu 3378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-reu 3381
This theorem is referenced by:  reueqd  3421  sbcreu  3876  oawordeu  8593  xpf1o  9179  dfac2b  10171  creur  12260  creui  12261  divalg  16440  divalg2  16442  lubfval  18395  lubeldm  18398  lubval  18401  glbfval  18408  glbeldm  18411  glbval  18414  joineu  18427  meeteu  18441  dfod2  19582  ustuqtop  24255  addsq2reu  27484  addsqn2reu  27485  addsqrexnreu  27486  addsqnreup  27487  2sqreulem1  27490  2sqreunnlem1  27493  usgredg2vtxeuALT  29239  isfrgr  30279  frcond1  30285  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  3vfriswmgr  30297  n4cyclfrgr  30310  eulplig  30504  riesz4  32083  cnlnadjeu  32097  poimirlem25  37652  poimirlem26  37653  hdmap1eulem  41824  hdmap1eulemOLDN  41825  hdmap14lem6  41875  reuf1odnf  47119  euoreqb  47121  isuspgrim0  47872  isuspgrimlem  47874  joindm3  48866  meetdm3  48868  upciclem1  48923  upfval2  48934  upfval3  48935  isuplem  48936
  Copyright terms: Public domain W3C validator