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

Theorem rexbiia 2880
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 649 . 2  |-  ( ( x  e.  A  /\  ph )  <->  ( x  e.  A  /\  ps )
)
32rexbii2 2879 1  |-  ( E. x  e.  A  ph  <->  E. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    e. wcel 1904   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-rex 2762
This theorem is referenced by:  2rexbiia  2895  ceqsrexbv  3161  reu8  3222  f1oweALT  6796  reldm  6863  seqomlem2  7186  fofinf1o  7870  wdom2d  8113  unbndrank  8331  cfsmolem  8718  fin1a2lem5  8852  fin1a2lem6  8853  infm3  10590  wwlktovfo  13108  znf1o  19199  lmres  20393  ist1-2  20440  itg2monolem1  22787  lhop1lem  23044  elaa  23348  ulmcau  23429  reeff1o  23481  recosf1o  23563  chpo1ubb  24398  istrkg2ld  24587  wlknwwlknsur  25519  wlkiswwlksur  25526  wwlkextsur  25538  nmopnegi  27699  nmop0  27720  nmfn0  27721  adjbd1o  27819  atom1d  28087  abfmpunirn  28327  rearchi  28679  eulerpartgbij  29278  eulerpartlemgh  29284  subfacp1lem3  29977  dfrdg2  30513  heiborlem7  32213  eq0rabdioph  35690  elicores  37731  fourierdlem70  38152  fourierdlem80  38162  ovolval3  38587  rexrsb  38735
  Copyright terms: Public domain W3C validator