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

Theorem eubidv 2647
 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 1928 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 eubi 2644 . 2 (∀𝑥(𝜓𝜒) → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  ∃!weu 2628 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2598  df-eu 2629 This theorem is referenced by:  euorv  2673  euanv  2686  reubidva  3342  reueq1  3361  reueubd  3382  eueq2  3651  eueq3  3652  moeq3  3653  reusv2lem2  5269  reusv2lem5  5272  reuhypd  5289  feu  6536  dff3  6853  dff4  6854  omxpenlem  8619  dfac5lem5  9556  dfac5  9557  kmlem2  9580  kmlem12  9590  kmlem13  9591  initoval  17269  termoval  17270  isinito  17272  istermo  17273  initoid  17277  termoid  17278  initoeu1  17283  initoeu2  17288  termoeu1  17290  upxp  22269  edgnbusgreu  27201  nbusgredgeu0  27202  frgrncvvdeqlem2  28129  bnj852  32369  bnj1489  32504  funpartfv  33666  fsuppind  39624  fourierdlem36  42953  aiotaval  43818  eu2ndop1stv  43849  dfdfat2  43852  tz6.12-afv  43897  tz6.12-afv2  43964  dfatcolem  43979  prprsprreu  44204  prprreueq  44205  setrec2lem1  45389
 Copyright terms: Public domain W3C validator