Theorem rexbiia 3040

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

Step	Hyp	Ref	Expression
1		rexbiia.1	. . 3 |- ( x e. A -> ( ph <-> ps ) )
2	1	pm5.32i 669	. 2 |- ( ( x e. A /\ ph ) <-> ( x e. A /\ ps ) )
3	2	rexbii2 3039	1 |- ( E. x e. A ph <-> E. x e. A ps )

Syntax hints:   -> wi 4   <-> wb 196   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  2rexbiia  3055  ceqsrexbv  3337  reu8  3402  f1oweALT  7152  reldm  7219  seqomlem2  7546  fofinf1o  8241  wdom2d  8485  unbndrank  8705  cfsmolem  9092  fin1a2lem5  9226  fin1a2lem6  9227  infm3  10982  wwlktovfo  13701  even2n  15066  znf1o  19900  lmres  21104  ist1-2  21151  itg2monolem1  23517  lhop1lem  23776  elaa  24071  ulmcau  24149  reeff1o  24201  recosf1o  24281  chpo1ubb  25170  istrkg2ld  25359  wlkpwwlkf1ouspgr  26765  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnextsur  26795  nmopnegi  28824  nmop0  28845  nmfn0  28846  adjbd1o  28944  atom1d  29212  abfmpunirn  29452  rearchi  29842  eulerpartgbij  30434  eulerpartlemgh  30440  subfacp1lem3  31164  dfrdg2  31701  heiborlem7  33616  qsresid  34096  eq0rabdioph  37340  elicores  39760  fourierdlem70  40393  fourierdlem80  40403  ovolval3  40861  rexrsb  41169