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

Theorem reubidva 3101
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 1829 . 2 𝑥𝜑
2 reubidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2reubida 3100 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wcel 1976  ∃!wreu 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-nf 1700  df-eu 2461  df-reu 2902
This theorem is referenced by:  reubidv  3102  reuxfr2d  4811  reuxfrd  4813  exfo  6269  f1ofveu  6521  zmax  11619  zbtwnre  11620  rebtwnz  11621  icoshftf1o  12124  divalgb  14913  1arith2  15418  ply1divalg2  23646  frg2woteu  26375  numclwwlk2lem1  26422  numclwlk2lem2f1o  26425  pjhtheu2  27452  reuxfr3d  28506  reuxfr4d  28507  xrsclat  28804  xrmulc1cn  29097  poimirlem25  32387  hdmap14lem14  35974  frgr2wwlkeu  41473  av-numclwwlk2lem1  41513  av-numclwlk2lem2f1o  41516
  Copyright terms: Public domain W3C validator