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

Theorem reubidva 3396
Description: Formula-building rule for restricted existential uniqueness 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 2586 . 2 (𝜑 → (∃!𝑥(𝑥𝐴𝜓) ↔ ∃!𝑥(𝑥𝐴𝜒)))
4 df-reu 3381 . 2 (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥(𝑥𝐴𝜓))
5 df-reu 3381 . 2 (∃!𝑥𝐴 𝜒 ↔ ∃!𝑥(𝑥𝐴𝜒))
63, 4, 53bitr4g 314 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2108  ∃!weu 2568  ∃!wreu 3378
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-reu 3381
This theorem is referenced by:  reubidv  3398  reuxfrd  3754  reuxfr1d  3756  fdmeu  6965  exfo  7125  f1ofveu  7425  zmax  12987  zbtwnre  12988  rebtwnz  12989  icoshftf1o  13514  divalgb  16441  1arith2  16966  ply1divalg2  26178  addsq2reu  27484  addsqn2reu  27485  addsqrexnreu  27486  2sqreultlem  27491  2sqreunnltlem  27494  frgr2wwlkeu  30346  numclwwlk2lem1  30395  numclwlk2lem2f1o  30398  pjhtheu2  31435  reuxfrdf  32510  xrsclat  33013  xrmulc1cn  33929  ply1divalg3  35647  poimirlem25  37652  hdmap14lem14  41883  cantnf2  43338  prproropreud  47496  quad1  47607  requad1  47609  requad2  47610  isuspgrim0lem  47871  isuspgrim0  47872  isuspgrimlem  47874  itscnhlinecirc02p  48706  reuxfr1dd  48726
  Copyright terms: Public domain W3C validator