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

Theorem reubidv 3301
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 484 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3300 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wcel 2110  ∃!wreu 3063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-mo 2539  df-eu 2568  df-reu 3068
This theorem is referenced by:  reueqd  3327  sbcreu  3788  oawordeu  8283  xpf1o  8808  dfac2b  9744  creur  11824  creui  11825  divalg  15964  divalg2  15966  lubfval  17856  lubeldm  17859  lubval  17862  glbfval  17869  glbeldm  17872  glbval  17875  joineu  17888  meeteu  17902  dfod2  18955  ustuqtop  23144  addsq2reu  26321  addsqn2reu  26322  addsqrexnreu  26323  addsqnreup  26324  2sqreulem1  26327  2sqreunnlem1  26330  usgredg2vtxeuALT  27310  isfrgr  28343  frcond1  28349  frgr1v  28354  nfrgr2v  28355  frgr3v  28358  3vfriswmgr  28361  n4cyclfrgr  28374  eulplig  28566  riesz4  30145  cnlnadjeu  30159  poimirlem25  35539  poimirlem26  35540  hdmap1eulem  39573  hdmap1eulemOLDN  39574  hdmap14lem6  39624  reuf1odnf  44271  euoreqb  44273  joindm3  45936  meetdm3  45938
  Copyright terms: Public domain W3C validator