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

Theorem reubidv 2967
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 463 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32reubidva 2966 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1826   E!wreu 2734
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-12 1862
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-nf 1625  df-eu 2222  df-reu 2739
This theorem is referenced by:  reueqd  2989  sbcreu  3329  oawordeu  7122  xpf1o  7598  dfac2  8424  creur  10446  creui  10447  divalg  14063  divalg2  14065  lubfval  15725  lubeldm  15728  lubval  15731  glbfval  15738  glbeldm  15741  glbval  15744  joineu  15757  meeteu  15771  dfod2  16703  ustuqtop  20834  isfrgra  25111  frgraunss  25116  frgra1v  25119  frgra2v  25120  frgra3v  25123  3vfriswmgra  25126  n4cyclfrgra  25139  riesz4  27099  cnlnadjeu  27113  hdmap1eulem  37964  hdmap1eulemOLDN  37965  hdmap14lem6  38016
  Copyright terms: Public domain W3C validator