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

Theorem rexbiia 2738
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 630 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2734 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-rex 2711
This theorem is referenced by:  2rexbiia  2739  ceqsrexbv  3083  reu8  3144  f1oweALT  6550  reldm  6614  seqomlem2  6892  fofinf1o  7580  wdom2d  7783  unbndrank  8037  cfsmolem  8427  fin1a2lem5  8561  fin1a2lem6  8562  infm3  10276  znf1o  17825  lmres  18745  ist1-2  18792  itg2monolem1  21069  lhop1lem  21326  elaa  21666  ulmcau  21744  reeff1o  21796  recosf1o  21875  chpo1ubb  22614  nmopnegi  25191  nmop0  25212  nmfn0  25213  adjbd1o  25311  atom1d  25579  abfmpunirn  25790  rearchi  26163  eulerpartgbij  26602  eulerpartlemgh  26608  subfacp1lem3  26917  dfrdg2  27455  heiborlem7  28557  eq0rabdioph  28957  rexrsb  29836  wwlktovfo  30096  wlknwwlknsur  30187  wlkiswwlksur  30194  wwlkextsur  30206
  Copyright terms: Public domain W3C validator