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

Theorem reubii 2837
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 2836 1  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1717   E!wreu 2651
This theorem is referenced by:  2reu5lem1  3082  reusv2lem5  4668  reusv2  4669  reusv5OLD  4673  reusv7OLD  4675  oaf1o  6742  aceq2  7933  spwex  14588  usgraidx2vlem1  21276  usgraidx2vlem2  21277  cnlnadjlem3  23420  disjrdx  23874  2reu7  27637  2reu8  27638  frgraunss  27748  frgraun  27749  n4cyclfrgra  27771  lshpsmreu  29224
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-tru 1325  df-ex 1548  df-nf 1551  df-eu 2242  df-reu 2656
  Copyright terms: Public domain W3C validator