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

Theorem eubidv 2284
Description: Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
Hypothesis
Ref Expression
eubidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
eubidv  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem eubidv
StepHypRef Expression
1 nfv 1751 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2282 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E!weu 2263
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664  df-eu 2267
This theorem is referenced by:  eubii  2286  eueq2  3242  eueq3  3243  moeq3  3245  reusv2lem2  4618  reusv2lem5  4621  reuhypd  4640  feu  5767  dff3  6041  dff4  6042  omxpenlem  7670  dfac5lem5  8547  dfac5  8548  kmlem2  8570  kmlem12  8580  kmlem13  8581  initoval  15844  termoval  15845  isinito  15847  istermo  15848  initoid  15852  termoid  15853  initoeu1  15858  initoeu2  15863  termoeu1  15865  upxp  20575  frgrancvvdeqlem3  25646  frgraeu  25668  bnj852  29561  bnj1489  29694  funpartfv  30538  fourierdlem36  37622  eu2ndop1stv  38071  dfdfat2  38080  tz6.12-afv  38122
  Copyright terms: Public domain W3C validator