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

Theorem reubidv 3343
 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 3342 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  ∃!wreu 3108 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598  df-eu 2629  df-reu 3113 This theorem is referenced by:  reueqd  3367  sbcreu  3807  oawordeu  8182  xpf1o  8681  dfac2b  9559  creur  11637  creui  11638  divalg  15764  divalg2  15766  lubfval  17600  lubeldm  17603  lubval  17606  glbfval  17613  glbeldm  17616  glbval  17619  joineu  17632  meeteu  17646  dfod2  18704  ustuqtop  22893  addsq2reu  26068  addsqn2reu  26069  addsqrexnreu  26070  addsqnreup  26071  2sqreulem1  26074  2sqreunnlem1  26077  usgredg2vtxeuALT  27056  isfrgr  28089  frcond1  28095  frgr1v  28100  nfrgr2v  28101  frgr3v  28104  3vfriswmgr  28107  n4cyclfrgr  28120  eulplig  28312  riesz4  29891  cnlnadjeu  29905  poimirlem25  35233  poimirlem26  35234  hdmap1eulem  39269  hdmap1eulemOLDN  39270  hdmap14lem6  39320  reuf1odnf  43831  euoreqb  43833
 Copyright terms: Public domain W3C validator