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

Theorem reubidva 3392
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
rmobidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
reubidva (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem reubidva
StepHypRef Expression
1 rmobidva.1 . . . 4 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 579 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32eubidv 2580 . 2 (𝜑 → (∃!𝑥(𝑥𝐴𝜓) ↔ ∃!𝑥(𝑥𝐴𝜒)))
4 df-reu 3377 . 2 (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥(𝑥𝐴𝜓))
5 df-reu 3377 . 2 (∃!𝑥𝐴 𝜒 ↔ ∃!𝑥(𝑥𝐴𝜒))
63, 4, 53bitr4g 313 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2106  ∃!weu 2562  ∃!wreu 3374
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534  df-eu 2563  df-reu 3377
This theorem is referenced by:  reubidv  3394  reuxfrd  3744  reuxfr1d  3746  exfo  7106  f1ofveu  7405  zmax  12931  zbtwnre  12932  rebtwnz  12933  icoshftf1o  13453  divalgb  16349  1arith2  16863  ply1divalg2  25663  addsq2reu  26950  addsqn2reu  26951  addsqrexnreu  26952  2sqreultlem  26957  2sqreunnltlem  26960  frgr2wwlkeu  29618  numclwwlk2lem1  29667  numclwlk2lem2f1o  29670  pjhtheu2  30707  reuxfrdf  31769  xrsclat  32219  xrmulc1cn  32979  poimirlem25  36599  hdmap14lem14  40838  cantnf2  42157  prproropreud  46256  quad1  46367  requad1  46369  requad2  46370  itscnhlinecirc02p  47549
  Copyright terms: Public domain W3C validator