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

Theorem reubidv 2809
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.)
Hypothesis
Ref Expression
reubidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
reubidv  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem reubidv
StepHypRef Expression
1 reubidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32reubidva 2808 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1715   E!wreu 2630
This theorem is referenced by:  reueqd  2831  sbcreug  3153  reusv6OLD  4648  reusv7OLD  4649  riotabidv  6448  oawordeu  6695  xpf1o  7166  dfac2  7904  creur  9887  creui  9888  divalg  12810  divalg2  12812  spwpr4  14550  dfod2  15087  riesz4  23078  cnlnadjeu  23092  ustuqtop  23870  isfrgra  27814  frgraunss  27819  frgra1v  27822  frgra3v  27826  3vfriswmgra  27829  n4cyclfrgra  27842  hdmap1eulem  32073  hdmap1eulemOLDN  32074  hdmap14lem6  32125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-nf 1550  df-eu 2221  df-reu 2635
  Copyright terms: Public domain W3C validator