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

Theorem reubidva 3102
 Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.)
Hypothesis
Ref Expression
reubidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
reubidva (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidva
StepHypRef Expression
1 nfv 1830 . 2 𝑥𝜑
2 reubidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2reubida 3101 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∈ wcel 1977  ∃!wreu 2898 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701  df-eu 2462  df-reu 2903 This theorem is referenced by:  reubidv  3103  reuxfr2d  4817  reuxfrd  4819  exfo  6285  f1ofveu  6544  zmax  11661  zbtwnre  11662  rebtwnz  11663  icoshftf1o  12166  divalgb  14965  1arith2  15470  ply1divalg2  23702  frg2woteu  26582  numclwwlk2lem1  26629  numclwlk2lem2f1o  26632  pjhtheu2  27659  reuxfr3d  28713  reuxfr4d  28714  xrsclat  29011  xrmulc1cn  29304  poimirlem25  32604  hdmap14lem14  36191  frgr2wwlkeu  41492  av-numclwwlk2lem1  41532  av-numclwlk2lem2f1o  41535
 Copyright terms: Public domain W3C validator