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

Theorem eubidv 2634
Description: Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)
Hypothesis
Ref Expression
eubidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
eubidv (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eubidv
StepHypRef Expression
1 eubidv.1 . . 3 (𝜑 → (𝜓𝜒))
21alrimiv 1909 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 eubi 2631 . 2 (∀𝑥(𝜓𝜒) → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1523  ∃!weu 2613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-mo 2578  df-eu 2614
This theorem is referenced by:  euorv  2665  euanv  2680  reubidva  3349  reueq1  3369  reueubd  3398  eueq2  3642  eueq3  3643  moeq3  3644  reusv2lem2  5198  reusv2lem5  5201  reuhypd  5218  feu  6429  dff3  6736  dff4  6737  omxpenlem  8472  dfac5lem5  9406  dfac5  9407  kmlem2  9430  kmlem12  9440  kmlem13  9441  initoval  17090  termoval  17091  isinito  17093  istermo  17094  initoid  17098  termoid  17099  initoeu1  17104  initoeu2  17109  termoeu1  17111  upxp  21919  edgnbusgreu  26836  nbusgredgeu0  26837  frgrncvvdeqlem2  27767  bnj852  31805  bnj1489  31938  funpartfv  33017  fourierdlem36  41992  aiotaval  42831  eu2ndop1stv  42862  dfdfat2  42865  tz6.12-afv  42910  tz6.12-afv2  42977  dfatcolem  42992  prprsprreu  43185  prprreueq  43186  setrec2lem1  44298
  Copyright terms: Public domain W3C validator