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

Theorem eubidv 2217
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 1619 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2216 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E!weu 2209
This theorem is referenced by:  eubii  2218  eueq2  3015  eueq3  3016  moeq3  3018  reusv2lem2  4618  reusv2lem5  4621  reusv7OLD  4628  reuhypd  4643  feu  5500  dff3  5756  dff4  5757  riotaeqdv  6392  omxpenlem  7051  dfac5lem5  7844  dfac5  7845  kmlem2  7867  kmlem12  7877  kmlem13  7878  upxp  17423  funpartfv  25042  eu2ndop1stv  27303  dfdfat2  27319  tz6.12-afv  27361  frgrancvvdeqlem3  27865  bnj852  28715  bnj1489  28848
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545  df-eu 2213
  Copyright terms: Public domain W3C validator