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

Theorem reubidva 2834
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 1626 . 2  |-  F/ x ph
2 reubidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2reubida 2833 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 1717   E!wreu 2651
This theorem is referenced by:  reubidv  2835  reuxfr2d  4686  reuxfrd  4688  exfo  5826  riotabidva  6502  f1ofveu  6520  zmax  10503  zbtwnre  10504  rebtwnz  10505  icoshftf1o  10952  divalgb  12851  1arith2  13223  ply1divalg2  19928  addinv  21788  pjhtheu2  22766  reuxfr3d  23820  reuxfr4d  23821  xrmulc1cn  24120  hdmap14lem14  31999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-eu 2242  df-reu 2656
  Copyright terms: Public domain W3C validator