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

Theorem eubidv 2151
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 1605 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2150 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E!weu 2143
This theorem is referenced by:  eubii  2152  eueq2  2939  eueq3  2940  moeq3  2942  reusv2lem2  4536  reusv2lem5  4539  reusv7OLD  4546  reuhypd  4561  feu  5417  dff3  5673  dff4  5674  riotaeqdv  6305  omxpenlem  6963  dfac5lem5  7754  dfac5  7755  kmlem2  7777  kmlem12  7787  kmlem13  7788  upxp  17317  dfdfat2  27994  tz6.12-afv  28035  bnj852  28953  bnj1489  29086
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532  df-eu 2147
  Copyright terms: Public domain W3C validator