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

Theorem reubidv 2860
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 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32reubidva 2859 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1721   E!wreu 2676
This theorem is referenced by:  reueqd  2882  sbcreug  3205  reusv6OLD  4701  reusv7OLD  4702  riotabidv  6518  oawordeu  6765  xpf1o  7236  dfac2  7975  creur  9958  creui  9959  divalg  12886  divalg2  12888  spwpr4  14626  dfod2  15163  ustuqtop  18237  riesz4  23528  cnlnadjeu  23542  isfrgra  28102  frgraunss  28107  frgra1v  28110  frgra3v  28114  3vfriswmgra  28117  n4cyclfrgra  28130  hdmap1eulem  32319  hdmap1eulemOLDN  32320  hdmap14lem6  32371
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-an 361  df-ex 1548  df-nf 1551  df-eu 2266  df-reu 2681
  Copyright terms: Public domain W3C validator