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

Theorem reubidva 2902
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.)
Hypothesis
Ref Expression
reubidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
reubidva  |-  ( 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 reubidva
StepHypRef Expression
1 nfv 1673 . 2  |-  F/ x ph
2 reubidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2reubida 2901 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1756   E!wreu 2715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-eu 2257  df-reu 2720
This theorem is referenced by:  reubidv  2903  reuxfr2d  4513  reuxfrd  4515  exfo  5859  f1ofveu  6084  zmax  10948  zbtwnre  10949  rebtwnz  10950  icoshftf1o  11406  divalgb  13606  1arith2  13987  ply1divalg2  21608  addinv  23837  pjhtheu2  24817  reuxfr3d  25871  reuxfr4d  25872  xrsclat  26139  xrmulc1cn  26358  frg2woteu  30645  numclwwlk2lem1  30692  numclwlk2lem2f1o  30695  hdmap14lem14  35526
  Copyright terms: Public domain W3C validator