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

Theorem eubidv 2291
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 1630 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2290 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   E!weu 2283
This theorem is referenced by:  eubii  2292  eueq2  3110  eueq3  3111  moeq3  3113  reusv2lem2  4728  reusv2lem5  4731  reusv7OLD  4738  reuhypd  4753  feu  5622  dff3  5885  dff4  5886  riotaeqdv  6553  omxpenlem  7212  dfac5lem5  8013  dfac5  8014  kmlem2  8036  kmlem12  8046  kmlem13  8047  upxp  17660  funpartfv  25795  eu2ndop1stv  27970  dfdfat2  27985  tz6.12-afv  28027  frgrancvvdeqlem3  28495  frgraeu  28517  bnj852  29366  bnj1489  29499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555  df-eu 2287
  Copyright terms: Public domain W3C validator