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

Theorem eubidv 2298
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 1683 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2296 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E!weu 2275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600  df-eu 2279
This theorem is referenced by:  eubii  2300  eueq2  3277  eueq3  3278  moeq3  3280  reusv2lem2  4649  reusv2lem5  4652  reusv7OLD  4659  reuhypd  4674  feu  5761  dff3  6035  dff4  6036  omxpenlem  7619  dfac5lem5  8509  dfac5  8510  kmlem2  8532  kmlem12  8542  kmlem13  8543  upxp  19951  frgrancvvdeqlem3  24806  frgraeu  24828  funpartfv  29448  fourierdlem36  31670  fourierdlem54  31688  eu2ndop1stv  31901  dfdfat2  31910  tz6.12-afv  31952  bnj852  33275  bnj1489  33408
  Copyright terms: Public domain W3C validator