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

Theorem reubidva 3265
 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 1993 . 2 𝑥𝜑
2 reubidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2reubida 3264 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∈ wcel 2140  ∃!wreu 3053 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-12 2197 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-nf 1859  df-eu 2612  df-reu 3058 This theorem is referenced by:  reubidv  3266  reuxfr2d  5041  reuxfrd  5043  exfo  6542  f1ofveu  6810  zmax  11999  zbtwnre  12000  rebtwnz  12001  icoshftf1o  12509  divalgb  15350  1arith2  15855  ply1divalg2  24118  frgr2wwlkeu  27503  numclwwlk2lem1  27559  numclwlk2lem2f1o  27562  numclwwlk2lem1OLD  27566  numclwlk2lem2f1oOLD  27569  pjhtheu2  28606  reuxfr3d  29659  reuxfr4d  29660  xrsclat  30011  xrmulc1cn  30307  poimirlem25  33766  hdmap14lem14  37694
 Copyright terms: Public domain W3C validator