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

Theorem eubidv 2489
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 1840 . 2 𝑥𝜑
2 eubidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2eubid 2487 1 (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  ∃!weu 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707  df-eu 2473
This theorem is referenced by:  eubii  2491  eueq2  3362  eueq3  3363  moeq3  3365  reusv2lem2  4829  reusv2lem2OLD  4830  reusv2lem5  4833  reuhypd  4855  feu  6037  dff3  6328  dff4  6329  omxpenlem  8005  dfac5lem5  8894  dfac5  8895  kmlem2  8917  kmlem12  8927  kmlem13  8928  initoval  16568  termoval  16569  isinito  16571  istermo  16572  initoid  16576  termoid  16577  initoeu1  16582  initoeu2  16587  termoeu1  16589  upxp  21336  edgnbusgreu  26156  frgrncvvdeqlem3  27029  frgreu  27049  bnj852  30699  bnj1489  30832  funpartfv  31694  fourierdlem36  39667  eu2ndop1stv  40506  dfdfat2  40515  tz6.12-afv  40557  setrec2lem1  41733
  Copyright terms: Public domain W3C validator