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

Theorem eubidv 2518
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 1883 . 2 𝑥𝜑
2 eubidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eubid 2516 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  ∃!weu 2498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-eu 2502
This theorem is referenced by:  eubii  2520  reueubd  3194  eueq2  3413  eueq3  3414  moeq3  3416  reusv2lem2  4899  reusv2lem2OLD  4900  reusv2lem5  4903  reuhypd  4925  feu  6118  dff3  6412  dff4  6413  omxpenlem  8102  dfac5lem5  8988  dfac5  8989  kmlem2  9011  kmlem12  9021  kmlem13  9022  initoval  16694  termoval  16695  isinito  16697  istermo  16698  initoid  16702  termoid  16703  initoeu1  16708  initoeu2  16713  termoeu1  16715  upxp  21474  edgnbusgreu  26313  nbusgredgeu0  26314  frgrncvvdeqlem2  27280  bnj852  31117  bnj1489  31250  funpartfv  32177  fourierdlem36  40678  eu2ndop1stv  41523  dfdfat2  41532  tz6.12-afv  41574  setrec2lem1  42765
  Copyright terms: Public domain W3C validator