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

Theorem reubidva 2990
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 1728 . 2  |-  F/ x ph
2 reubidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2reubida 2989 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 367    e. wcel 1842   E!wreu 2755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-12 1878
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638  df-eu 2242  df-reu 2760
This theorem is referenced by:  reubidv  2991  reuxfr2d  4613  reuxfrd  4615  exfo  6026  f1ofveu  6272  zmax  11223  zbtwnre  11224  rebtwnz  11225  icoshftf1o  11695  divalgb  14269  1arith2  14653  ply1divalg2  22829  frg2woteu  25459  numclwwlk2lem1  25506  numclwlk2lem2f1o  25509  addinv  25754  pjhtheu2  26734  reuxfr3d  27789  reuxfr4d  27790  xrsclat  28106  xrmulc1cn  28351  hdmap14lem14  34884
  Copyright terms: Public domain W3C validator