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

Theorem rexbiia 2865
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 2860 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 1758   E.wrex 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-rex 2802
This theorem is referenced by:  2rexbiia  2867  ceqsrexbv  3195  reu8  3256  f1oweALT  6666  reldm  6730  seqomlem2  7011  fofinf1o  7698  wdom2d  7901  unbndrank  8155  cfsmolem  8545  fin1a2lem5  8679  fin1a2lem6  8680  infm3  10395  znf1o  18104  lmres  19031  ist1-2  19078  itg2monolem1  21356  lhop1lem  21613  elaa  21910  ulmcau  21988  reeff1o  22040  recosf1o  22119  chpo1ubb  22858  istrkg2ld  23050  nmopnegi  25516  nmop0  25537  nmfn0  25538  adjbd1o  25636  atom1d  25904  abfmpunirn  26113  rearchi  26450  eulerpartgbij  26894  eulerpartlemgh  26900  subfacp1lem3  27209  dfrdg2  27748  heiborlem7  28859  eq0rabdioph  29258  rexrsb  30136  wwlktovfo  30396  wlknwwlknsur  30487  wlkiswwlksur  30494  wwlkextsur  30506
  Copyright terms: Public domain W3C validator