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

Theorem reubidv 2898
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 453 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32reubidva 2897 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    e. wcel 1727   E!wreu 2713
This theorem is referenced by:  reueqd  2920  sbcreu  3252  sbcreugOLD  3253  reusv6OLD  4763  reusv7OLD  4764  riotabidv  6580  oawordeu  6827  xpf1o  7298  dfac2  8042  creur  10025  creui  10026  divalg  12954  divalg2  12956  spwpr4  14694  dfod2  15231  ustuqtop  18307  riesz4  23598  cnlnadjeu  23612  isfrgra  28478  frgraunss  28483  frgra1v  28486  frgra3v  28490  3vfriswmgra  28493  n4cyclfrgra  28506  hdmap1eulem  32720  hdmap1eulemOLDN  32721  hdmap14lem6  32772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-11 1763
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-eu 2291  df-reu 2718
  Copyright terms: Public domain W3C validator