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

Theorem rexbiia 2589
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
ralbiia.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 ralbiia.1 . . 3  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
21pm5.32i 618 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2585 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  2rexbiia  2590  ceqsrexbv  2915  reu8  2974  f1oweALT  5867  reldm  6187  seqomlem2  6479  fofinf1o  7153  wdom2d  7310  unbndrank  7530  cfsmolem  7912  fin1a2lem5  8046  fin1a2lem6  8047  infm3  9729  znf1o  16521  lmres  17044  ist1-2  17091  itg2monolem1  19121  lhop1lem  19376  elaa  19712  ulmcau  19788  reeff1o  19839  recosf1o  19913  chpo1ubb  20646  nmopnegi  22561  nmop0  22582  nmfn0  22583  adjbd1o  22681  atom1d  22949  abfmpunirn  23231  subfacp1lem3  23728  dfrdg2  24223  heiborlem7  26644  eq0rabdioph  26959  rexrsb  28050
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-rex 2562
  Copyright terms: Public domain W3C validator