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

Theorem reubii 3048
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 3047 1  |-  ( E! x  e.  A  ph  <->  E! x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   E!wreu 2816
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-eu 2279  df-reu 2821
This theorem is referenced by:  2reu5lem1  3309  reusv2lem5  4652  reusv2  4653  reusv5OLD  4657  reusv7OLD  4659  oaf1o  7212  aceq2  8500  lubfval  15465  lubeldm  15468  glbfval  15478  glbeldm  15481  oduglb  15626  odulub  15628  usgraidx2vlem1  24095  usgraidx2vlem2  24096  frgraunss  24699  frgraun  24700  n4cyclfrgra  24722  cnlnadjlem3  26692  disjrdx  27151  2reu7  31691  2reu8  31692  usgedgvadf1lem1  31908  usgedgvadf1lem2  31909  usgedgvadf1ALTlem1  31911  usgedgvadf1ALTlem2  31912  lshpsmreu  33924
  Copyright terms: Public domain W3C validator