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

Theorem reubidva 3307
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 13-Nov-2004.) Reduce axiom usage. (Revised by Wolf Lammen, 14-Jan-2023.)
Hypothesis
Ref Expression
reubidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
reubidva (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidva
StepHypRef Expression
1 reubidva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 575 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32eubidv 2626 . 2 (𝜑 → (∃!𝑥(𝑥𝐴𝜓) ↔ ∃!𝑥(𝑥𝐴𝜒)))
4 df-reu 3096 . 2 (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥(𝑥𝐴𝜓))
5 df-reu 3096 . 2 (∃!𝑥𝐴 𝜒 ↔ ∃!𝑥(𝑥𝐴𝜒))
63, 4, 53bitr4g 306 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  wcel 2157  ∃!weu 2608  ∃!wreu 3091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-mo 2591  df-eu 2609  df-reu 3096
This theorem is referenced by:  reubidv  3309  reuxfr2d  5089  reuxfrd  5091  exfo  6603  f1ofveu  6873  zmax  12030  zbtwnre  12031  rebtwnz  12032  icoshftf1o  12547  divalgb  15463  1arith2  15965  ply1divalg2  24239  frgr2wwlkeu  27676  numclwwlk2lem1  27749  numclwlk2lem2f1o  27752  numclwlk2lem2f1oOLD  27755  numclwwlk2lem1OLD  27760  numclwlk2lem2f1oOLDOLD  27763  pjhtheu2  28800  reuxfr3d  29852  reuxfr4d  29853  xrsclat  30196  xrmulc1cn  30492  poimirlem25  33923  hdmap14lem14  37902
  Copyright terms: Public domain W3C validator