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

Theorem eubidv 2285
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 1674 . 2  |-  F/ x ph
2 eubidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2eubid 2283 1  |-  ( ph  ->  ( E! x ps  <->  E! x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E!weu 2262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591  df-eu 2266
This theorem is referenced by:  eubii  2287  eueq2  3240  eueq3  3241  moeq3  3243  reusv2lem2  4605  reusv2lem5  4608  reusv7OLD  4615  reuhypd  4630  feu  5698  dff3  5968  dff4  5969  omxpenlem  7525  dfac5lem5  8411  dfac5  8412  kmlem2  8434  kmlem12  8444  kmlem13  8445  upxp  19331  funpartfv  28140  eu2ndop1stv  30194  dfdfat2  30205  tz6.12-afv  30247  frgrancvvdeqlem3  30793  frgraeu  30815  bnj852  32266  bnj1489  32399
  Copyright terms: Public domain W3C validator