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

Theorem reubidva 3038
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 1678 . 2  |-  F/ x ph
2 reubidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2reubida 3037 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 1762   E!wreu 2809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-12 1798
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595  df-eu 2272  df-reu 2814
This theorem is referenced by:  reubidv  3039  reuxfr2d  4663  reuxfrd  4665  exfo  6030  f1ofveu  6270  zmax  11168  zbtwnre  11169  rebtwnz  11170  icoshftf1o  11632  divalgb  13910  1arith2  14294  ply1divalg2  22267  frg2woteu  24718  numclwwlk2lem1  24765  numclwlk2lem2f1o  24768  addinv  25016  pjhtheu2  25996  reuxfr3d  27050  reuxfr4d  27051  xrsclat  27316  xrmulc1cn  27534  hdmap14lem14  36556
  Copyright terms: Public domain W3C validator