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

Theorem eubidv 2478
 Description: Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
Hypothesis
Ref Expression
eubidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
eubidv (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem eubidv
StepHypRef Expression
1 nfv 1830 . 2 𝑥𝜑
2 eubidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eubid 2476 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∃!weu 2458 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-eu 2462 This theorem is referenced by:  eubii  2480  eueq2  3347  eueq3  3348  moeq3  3350  reusv2lem2  4795  reusv2lem2OLD  4796  reusv2lem5  4799  reuhypd  4821  feu  5993  dff3  6280  dff4  6281  omxpenlem  7946  dfac5lem5  8833  dfac5  8834  kmlem2  8856  kmlem12  8866  kmlem13  8867  initoval  16470  termoval  16471  isinito  16473  istermo  16474  initoid  16478  termoid  16479  initoeu1  16484  initoeu2  16489  termoeu1  16491  upxp  21236  frgrancvvdeqlem3  26559  frgraeu  26581  bnj852  30245  bnj1489  30378  funpartfv  31222  fourierdlem36  39036  eu2ndop1stv  39851  dfdfat2  39860  tz6.12-afv  39902  edgnbusgreu  40595  frgrncvvdeqlem3  41471  frgreu  41491  setrec2lem1  42239
 Copyright terms: Public domain W3C validator