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

Theorem eubidv 2266
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 1626 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2265 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E!weu 2258
This theorem is referenced by:  eubii  2267  eueq2  3072  eueq3  3073  moeq3  3075  reusv2lem2  4688  reusv2lem5  4691  reusv7OLD  4698  reuhypd  4713  feu  5582  dff3  5845  dff4  5846  riotaeqdv  6513  omxpenlem  7172  dfac5lem5  7968  dfac5  7969  kmlem2  7991  kmlem12  8001  kmlem13  8002  upxp  17612  funpartfv  25702  eu2ndop1stv  27851  dfdfat2  27866  tz6.12-afv  27908  frgrancvvdeqlem3  28139  frgraeu  28161  bnj852  29002  bnj1489  29135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-eu 2262
  Copyright terms: Public domain W3C validator