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

Theorem rexbiia 2887
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 642 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2886 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    e. wcel 1886   E.wrex 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1663  df-rex 2742
This theorem is referenced by:  2rexbiia  2905  ceqsrexbv  3172  reu8  3233  f1oweALT  6774  reldm  6841  seqomlem2  7165  fofinf1o  7849  wdom2d  8092  unbndrank  8310  cfsmolem  8697  fin1a2lem5  8831  fin1a2lem6  8832  infm3  10565  wwlktovfo  13026  znf1o  19115  lmres  20309  ist1-2  20356  itg2monolem1  22701  lhop1lem  22958  elaa  23262  ulmcau  23343  reeff1o  23395  recosf1o  23477  chpo1ubb  24312  istrkg2ld  24501  wlknwwlknsur  25433  wlkiswwlksur  25440  wwlkextsur  25452  nmopnegi  27611  nmop0  27632  nmfn0  27633  adjbd1o  27731  atom1d  27999  abfmpunirn  28244  rearchi  28598  eulerpartgbij  29198  eulerpartlemgh  29204  subfacp1lem3  29898  dfrdg2  30435  heiborlem7  32142  eq0rabdioph  35613  elicores  37629  fourierdlem70  38034  fourierdlem80  38044  rexrsb  38584
  Copyright terms: Public domain W3C validator