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

Theorem reubidva 3393
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 579 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32eubidv 2667 . 2 (𝜑 → (∃!𝑥(𝑥𝐴𝜓) ↔ ∃!𝑥(𝑥𝐴𝜒)))
4 df-reu 3149 . 2 (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥(𝑥𝐴𝜓))
5 df-reu 3149 . 2 (∃!𝑥𝐴 𝜒 ↔ ∃!𝑥(𝑥𝐴𝜒))
63, 4, 53bitr4g 315 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2106  ∃!weu 2648  ∃!wreu 3144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-mo 2615  df-eu 2649  df-reu 3149
This theorem is referenced by:  reubidv  3394  reuxfrd  3742  reuxfr1d  3744  exfo  6866  f1ofveu  7146  zmax  12337  zbtwnre  12338  rebtwnz  12339  icoshftf1o  12853  divalgb  15747  1arith2  16256  ply1divalg2  24647  addsq2reu  25930  addsqn2reu  25931  addsqrexnreu  25932  2sqreultlem  25937  2sqreunnltlem  25940  frgr2wwlkeu  28021  numclwwlk2lem1  28070  numclwlk2lem2f1o  28073  pjhtheu2  29108  reuxfrdf  30170  xrsclat  30582  xrmulc1cn  31060  poimirlem25  34785  hdmap14lem14  38885  prproropreud  43500  quad1  43614  requad1  43616  requad2  43617  itscnhlinecirc02p  44601
  Copyright terms: Public domain W3C validator