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

Theorem eubidv 2627
 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 1992 . 2 𝑥𝜑
2 eubidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eubid 2625 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∃!weu 2607 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196 This theorem depends on definitions:  df-bi 197  df-ex 1854  df-nf 1859  df-eu 2611 This theorem is referenced by:  eubii  2629  reueubd  3303  eueq2  3521  eueq3  3522  moeq3  3524  reusv2lem2  5018  reusv2lem2OLD  5019  reusv2lem5  5022  reuhypd  5044  feu  6241  dff3  6536  dff4  6537  omxpenlem  8228  dfac5lem5  9160  dfac5  9161  kmlem2  9185  kmlem12  9195  kmlem13  9196  initoval  16868  termoval  16869  isinito  16871  istermo  16872  initoid  16876  termoid  16877  initoeu1  16882  initoeu2  16887  termoeu1  16889  upxp  21648  edgnbusgreu  26488  nbusgredgeu0  26489  frgrncvvdeqlem2  27475  bnj852  31319  bnj1489  31452  funpartfv  32379  fourierdlem36  40881  eu2ndop1stv  41726  dfdfat2  41735  tz6.12-afv  41777  setrec2lem1  42968
 Copyright terms: Public domain W3C validator