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

Theorem reubidv 2852
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 2851 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 2668
This theorem is referenced by:  reueqd  2874  sbcreug  3197  reusv6OLD  4693  reusv7OLD  4694  riotabidv  6510  oawordeu  6757  xpf1o  7228  dfac2  7967  creur  9950  creui  9951  divalg  12878  divalg2  12880  spwpr4  14618  dfod2  15155  ustuqtop  18229  riesz4  23520  cnlnadjeu  23534  isfrgra  28094  frgraunss  28099  frgra1v  28102  frgra3v  28106  3vfriswmgra  28109  n4cyclfrgra  28122  hdmap1eulem  32307  hdmap1eulemOLDN  32308  hdmap14lem6  32359
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 2258  df-reu 2673
  Copyright terms: Public domain W3C validator