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

Theorem rexbiia 2907
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
rexbiia.1  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rexbiia  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )

Proof of Theorem rexbiia
StepHypRef Expression
1 rexbiia.1 . . 3  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
21pm5.32i 637 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2906 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 186    e. wcel 1844   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654
This theorem depends on definitions:  df-bi 187  df-an 371  df-ex 1636  df-rex 2762
This theorem is referenced by:  2rexbiia  2925  ceqsrexbv  3186  reu8  3247  f1oweALT  6770  reldm  6837  seqomlem2  7155  fofinf1o  7837  wdom2d  8042  unbndrank  8294  cfsmolem  8684  fin1a2lem5  8818  fin1a2lem6  8819  infm3  10544  wwlktovfo  12954  znf1o  18890  lmres  20096  ist1-2  20143  itg2monolem1  22451  lhop1lem  22708  elaa  23006  ulmcau  23084  reeff1o  23136  recosf1o  23216  chpo1ubb  24049  istrkg2ld  24238  wlknwwlknsur  25141  wlkiswwlksur  25148  wwlkextsur  25160  nmopnegi  27310  nmop0  27331  nmfn0  27332  adjbd1o  27430  atom1d  27698  abfmpunirn  27946  rearchi  28298  eulerpartgbij  28830  eulerpartlemgh  28836  subfacp1lem3  29492  dfrdg2  30028  heiborlem7  31608  eq0rabdioph  35084  fourierdlem70  37340  fourierdlem80  37350  rexrsb  37555
  Copyright terms: Public domain W3C validator