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

Theorem reubidva 3155
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 1883 . 2 𝑥𝜑
2 reubidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2reubida 3154 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  ∃!wreu 2943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750  df-eu 2502  df-reu 2948
This theorem is referenced by:  reubidv  3156  reuxfr2d  4921  reuxfrd  4923  exfo  6417  f1ofveu  6685  zmax  11823  zbtwnre  11824  rebtwnz  11825  icoshftf1o  12333  divalgb  15174  1arith2  15679  ply1divalg2  23943  frgr2wwlkeu  27307  numclwwlk2lem1  27356  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2f1oOLD  27366  pjhtheu2  28403  reuxfr3d  29456  reuxfr4d  29457  xrsclat  29808  xrmulc1cn  30104  poimirlem25  33564  hdmap14lem14  37490
  Copyright terms: Public domain W3C validator