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

Theorem reubii 2739
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 2738 1  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1696   E!wreu 2558
This theorem is referenced by:  2reu5lem1  2983  reusv2lem5  4555  reusv2  4556  reusv5OLD  4560  reusv7OLD  4562  oaf1o  6577  aceq2  7762  spwex  14354  cnlnadjlem3  22665  disjrdx  23385  2reu7  28072  2reu8  28073  n4cyclfrgra  28440  lshpsmreu  29921
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-eu 2160  df-reu 2563
  Copyright terms: Public domain W3C validator