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 619 . 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 set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1725   E.wrex 2706
This theorem is referenced by:  2rexbiia  2739  ceqsrexbv  3070  reu8  3130  f1oweALT  6074  reldm  6398  seqomlem2  6708  fofinf1o  7387  wdom2d  7548  unbndrank  7768  cfsmolem  8150  fin1a2lem5  8284  fin1a2lem6  8285  infm3  9967  znf1o  16832  lmres  17364  ist1-2  17411  itg2monolem1  19642  lhop1lem  19897  elaa  20233  ulmcau  20311  reeff1o  20363  recosf1o  20437  chpo1ubb  21175  nmopnegi  23468  nmop0  23489  nmfn0  23490  adjbd1o  23588  atom1d  23856  abfmpunirn  24064  subfacp1lem3  24868  dfrdg2  25423  heiborlem7  26526  eq0rabdioph  26835  rexrsb  27923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-rex 2711
  Copyright terms: Public domain W3C validator