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

Theorem eubidv 2652
Description: Formula-building rule for unique existential 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 2008 . 2 𝑥𝜑
2 eubidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eubid 2650 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  ∃!weu 2632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-12 2216
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1865  df-eu 2636
This theorem is referenced by:  eubii  2654  reueubd  3352  eueq2  3575  eueq3  3576  moeq3  3578  reusv2lem2  5065  reusv2lem5  5068  reuhypd  5089  feu  6292  dff3  6591  dff4  6592  omxpenlem  8297  dfac5lem5  9230  dfac5  9231  kmlem2  9255  kmlem12  9265  kmlem13  9266  initoval  16847  termoval  16848  isinito  16850  istermo  16851  initoid  16855  termoid  16856  initoeu1  16861  initoeu2  16866  termoeu1  16868  upxp  21636  edgnbusgreu  26480  edgnbusgreuOLD  26481  nbusgredgeu0  26482  frgrncvvdeqlem2  27471  bnj852  31311  bnj1489  31444  funpartfv  32370  fourierdlem36  40836  aiotaval  41674  eu2ndop1stv  41711  dfdfat2  41714  tz6.12-afv  41759  tz6.12-afv2  41826  dfatcolem  41841  setrec2lem1  43005
  Copyright terms: Public domain W3C validator