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

Theorem rexbiia 2964
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 2963 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 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-rex 2820
This theorem is referenced by:  2rexbiia  2978  ceqsrexbv  3238  reu8  3299  f1oweALT  6765  reldm  6832  seqomlem2  7113  fofinf1o  7797  wdom2d  8002  unbndrank  8256  cfsmolem  8646  fin1a2lem5  8780  fin1a2lem6  8781  infm3  10498  wwlktovfo  12855  znf1o  18357  lmres  19567  ist1-2  19614  itg2monolem1  21892  lhop1lem  22149  elaa  22446  ulmcau  22524  reeff1o  22576  recosf1o  22655  chpo1ubb  23394  istrkg2ld  23586  wlknwwlknsur  24388  wlkiswwlksur  24395  wwlkextsur  24407  nmopnegi  26560  nmop0  26581  nmfn0  26582  adjbd1o  26680  atom1d  26948  abfmpunirn  27162  rearchi  27495  eulerpartgbij  27951  eulerpartlemgh  27957  subfacp1lem3  28266  dfrdg2  28805  heiborlem7  29916  eq0rabdioph  30314  fourierdlem70  31477  fourierdlem80  31487  rexrsb  31641
  Copyright terms: Public domain W3C validator