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

Theorem reubidva 3386
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 2665 . 2 (𝜑 → (∃!𝑥(𝑥𝐴𝜓) ↔ ∃!𝑥(𝑥𝐴𝜒)))
4 df-reu 3142 . 2 (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥(𝑥𝐴𝜓))
5 df-reu 3142 . 2 (∃!𝑥𝐴 𝜒 ↔ ∃!𝑥(𝑥𝐴𝜒))
63, 4, 53bitr4g 315 1 (𝜑 → (∃!𝑥𝐴 𝜓 ↔ ∃!𝑥𝐴 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105  ∃!weu 2646  ∃!wreu 3137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-mo 2615  df-eu 2647  df-reu 3142
This theorem is referenced by:  reubidv  3387  reuxfrd  3736  reuxfr1d  3738  exfo  6863  f1ofveu  7140  zmax  12333  zbtwnre  12334  rebtwnz  12335  icoshftf1o  12848  divalgb  15743  1arith2  16252  ply1divalg2  24659  addsq2reu  25943  addsqn2reu  25944  addsqrexnreu  25945  2sqreultlem  25950  2sqreunnltlem  25953  frgr2wwlkeu  28033  numclwwlk2lem1  28082  numclwlk2lem2f1o  28085  pjhtheu2  29120  reuxfrdf  30182  xrsclat  30594  xrmulc1cn  31072  poimirlem25  34798  hdmap14lem14  38897  prproropreud  43548  quad1  43662  requad1  43664  requad2  43665  itscnhlinecirc02p  44700
  Copyright terms: Public domain W3C validator