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

Theorem reubii 3041
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 3040 1  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1823   E!wreu 2806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-eu 2288  df-reu 2811
This theorem is referenced by:  2reu5lem1  3302  reusv2lem5  4642  reusv2  4643  reusv5OLD  4647  reusv7OLD  4649  oaf1o  7204  aceq2  8491  lubfval  15807  lubeldm  15810  glbfval  15820  glbeldm  15823  oduglb  15968  odulub  15970  usgraidx2vlem1  24593  usgraidx2vlem2  24594  frgraunss  25197  frgraun  25198  n4cyclfrgra  25220  cnlnadjlem3  27186  disjrdx  27661  2reu7  32435  2reu8  32436  usgedgvadf1lem1  32785  usgedgvadf1lem2  32786  usgedgvadf1ALTlem1  32788  usgedgvadf1ALTlem2  32789  lshpsmreu  35231
  Copyright terms: Public domain W3C validator