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

Theorem reubidva 3027
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 1694 . 2  |-  F/ x ph
2 reubidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2reubida 3026 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 1804   E!wreu 2795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604  df-eu 2272  df-reu 2800
This theorem is referenced by:  reubidv  3028  reuxfr2d  4660  reuxfrd  4662  exfo  6034  f1ofveu  6276  zmax  11190  zbtwnre  11191  rebtwnz  11192  icoshftf1o  11654  divalgb  14044  1arith2  14428  ply1divalg2  22517  frg2woteu  25033  numclwwlk2lem1  25080  numclwlk2lem2f1o  25083  addinv  25332  pjhtheu2  26312  reuxfr3d  27366  reuxfr4d  27367  xrsclat  27646  xrmulc1cn  27890  hdmap14lem14  37486
  Copyright terms: Public domain W3C validator