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

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

Proof of Theorem reubidv
StepHypRef Expression
1 reubidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 473 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3320 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wcel 2051  ∃!wreu 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-mo 2548  df-eu 2585  df-reu 3088
This theorem is referenced by:  reueqd  3352  sbcreu  3755  oawordeu  7980  xpf1o  8473  dfac2b  9348  creur  11431  creui  11432  divalg  15612  divalg2  15614  lubfval  17458  lubeldm  17461  lubval  17464  glbfval  17471  glbeldm  17474  glbval  17477  joineu  17490  meeteu  17504  dfod2  18464  ustuqtop  22573  addsq2reu  25733  addsqn2reu  25734  addsqrexnreu  25735  addsqnreup  25736  2sqreulem1  25739  2sqreunnlem1  25742  usgredg2vtxeuALT  26722  isfrgr  27807  frcond1  27815  frgr1v  27820  nfrgr2v  27821  frgr3v  27824  3vfriswmgr  27827  n4cyclfrgr  27840  eulplig  28054  riesz4  29637  cnlnadjeu  29651  poimirlem25  34395  poimirlem26  34396  hdmap1eulem  38440  hdmap1eulemOLDN  38441  hdmap14lem6  38491  reuf1odnf  42746  euoreqb  42748
  Copyright terms: Public domain W3C validator