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

Theorem reubii 2886
Description: Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 22-Oct-1999.)
Hypothesis
Ref Expression
reubii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
reubii  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )

Proof of Theorem reubii
StepHypRef Expression
1 reubii.1 . . 3  |-  ( ph  <->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
32reubiia 2885 1  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1725   E!wreu 2699
This theorem is referenced by:  2reu5lem1  3131  reusv2lem5  4720  reusv2  4721  reusv5OLD  4725  reusv7OLD  4727  oaf1o  6798  aceq2  7992  spwex  14653  usgraidx2vlem1  21402  usgraidx2vlem2  21403  cnlnadjlem3  23564  disjrdx  24023  2reu7  27926  2reu8  27927  frgraunss  28312  frgraun  28313  n4cyclfrgra  28335  lshpsmreu  29834
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-tru 1328  df-ex 1551  df-nf 1554  df-eu 2284  df-reu 2704
  Copyright terms: Public domain W3C validator