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

Theorem reubidva 3391
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 578 . . 3 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32eubidv 2579 . 2 (𝜑 → (∃!𝑥(𝑥𝐴𝜓) ↔ ∃!𝑥(𝑥𝐴𝜒)))
4 df-reu 3376 . 2 (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥(𝑥𝐴𝜓))
5 df-reu 3376 . 2 (∃!𝑥𝐴 𝜒 ↔ ∃!𝑥(𝑥𝐴𝜒))
63, 4, 53bitr4g 314 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wcel 2105  ∃!weu 2561  ∃!wreu 3373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-mo 2533  df-eu 2562  df-reu 3376
This theorem is referenced by:  reubidv  3393  reuxfrd  3744  reuxfr1d  3746  exfo  7106  f1ofveu  7406  zmax  12934  zbtwnre  12935  rebtwnz  12936  icoshftf1o  13456  divalgb  16352  1arith2  16866  ply1divalg2  25892  addsq2reu  27180  addsqn2reu  27181  addsqrexnreu  27182  2sqreultlem  27187  2sqreunnltlem  27190  frgr2wwlkeu  29848  numclwwlk2lem1  29897  numclwlk2lem2f1o  29900  pjhtheu2  30937  reuxfrdf  31999  xrsclat  32449  xrmulc1cn  33209  poimirlem25  36817  hdmap14lem14  41056  cantnf2  42378  prproropreud  46476  quad1  46587  requad1  46589  requad2  46590  itscnhlinecirc02p  47559
  Copyright terms: Public domain W3C validator