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

Theorem reubidva 2883
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 1629 . 2  |-  F/ x ph
2 reubidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2reubida 2882 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1725   E!wreu 2699
This theorem is referenced by:  reubidv  2884  reuxfr2d  4738  reuxfrd  4740  exfo  5879  riotabidva  6558  f1ofveu  6576  zmax  10563  zbtwnre  10564  rebtwnz  10565  icoshftf1o  11012  divalgb  12916  1arith2  13288  ply1divalg2  20053  addinv  21932  pjhtheu2  22910  reuxfr3d  23968  reuxfr4d  23969  xrmulc1cn  24308  frg2woteu  28381  hdmap14lem14  32619
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-eu 2284  df-reu 2704
  Copyright terms: Public domain W3C validator