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

Theorem rexbiia 2576
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 2572 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 1684   E.wrex 2544
This theorem is referenced by:  2rexbiia  2577  ceqsrexbv  2902  reu8  2961  f1oweALT  5851  reldm  6171  seqomlem2  6463  fofinf1o  7137  wdom2d  7294  unbndrank  7514  cfsmolem  7896  fin1a2lem5  8030  fin1a2lem6  8031  infm3  9713  znf1o  16505  lmres  17028  ist1-2  17075  itg2monolem1  19105  lhop1lem  19360  elaa  19696  ulmcau  19772  reeff1o  19823  recosf1o  19897  chpo1ubb  20630  nmopnegi  22545  nmop0  22566  nmfn0  22567  adjbd1o  22665  atom1d  22933  abfmpunirn  23216  subfacp1lem3  23713  dfrdg2  24152  heiborlem7  26541  eq0rabdioph  26856  rexrsb  27947
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator