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

Theorem reubii 2726
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 10 . 2  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
32reubiia 2725 1  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1684   E!wreu 2545
This theorem is referenced by:  2reu5lem1  2970  reusv2lem5  4539  reusv2  4540  reusv5OLD  4544  reusv7OLD  4546  oaf1o  6561  aceq2  7746  spwex  14338  cnlnadjlem3  22649  disjrdx  23370  2reu7  27969  2reu8  27970  lshpsmreu  29299
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-eu 2147  df-reu 2550
  Copyright terms: Public domain W3C validator