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

Theorem reubidv 3393
Description: Formula-building rule for restricted existential 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 481 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32reubidva 3391 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2106  ∃!wreu 3373
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 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2533  df-eu 2562  df-reu 3376
This theorem is referenced by:  reueqd  3418  sbcreu  3866  oawordeu  8538  xpf1o  9122  dfac2b  10107  creur  12188  creui  12189  divalg  16328  divalg2  16330  lubfval  18285  lubeldm  18288  lubval  18291  glbfval  18298  glbeldm  18301  glbval  18304  joineu  18317  meeteu  18331  dfod2  19396  ustuqtop  23680  addsq2reu  26870  addsqn2reu  26871  addsqrexnreu  26872  addsqnreup  26873  2sqreulem1  26876  2sqreunnlem1  26879  usgredg2vtxeuALT  28344  isfrgr  29378  frcond1  29384  frgr1v  29389  nfrgr2v  29390  frgr3v  29393  3vfriswmgr  29396  n4cyclfrgr  29409  eulplig  29601  riesz4  31180  cnlnadjeu  31194  poimirlem25  36317  poimirlem26  36318  hdmap1eulem  40498  hdmap1eulemOLDN  40499  hdmap14lem6  40549  reuf1odnf  45587  euoreqb  45589  joindm3  47250  meetdm3  47252
  Copyright terms: Public domain W3C validator