Theorem rexbii 2537

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
rexbii	|- ( E. x e. A ph <-> E. x e. A ps )

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 |- ( ph <-> ps )
2	1	a1i 9	. . 3 |- ( T. -> ( ph <-> ps ) )
3	2	rexbidv 2531	. 2 |- ( T. -> ( E. x e. A ph <-> E. x e. A ps ) )
4	3	mptru 1404	1 |- ( E. x e. A ph <-> E. x e. A ps )

Syntax hints:   <-> wb 105   T. wtru 1396   E.wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-rex 2514

This theorem is referenced by:  2rexbii  2539  r19.29r  2669  r19.42v  2688  rexcom13  2697  rexrot4  2698  3reeanv  2702  cbvrex2vw  2777  cbvrex2v  2779  rexcom4  2823  rexcom4a  2824  rexcom4b  2825  ceqsrex2v  2935  clel5  2940  reu7  2998  0el  3514  iuncom  3971  iuncom4  3972  iuniin  3975  dfiunv2  4001  iunab  4012  iunin2  4029  iundif2ss  4031  iunun  4044  iunxiun  4047  iunpwss  4057  inuni  4239  iunopab  4370  sucel  4501  iunpw  4571  xpiundi  4777  xpiundir  4778  reliin  4841  rexxpf  4869  iunxpf  4870  cnvuni  4908  dmiun  4932  dfima3  5071  rniun  5139  dminxp  5173  imaco  5234  coiun  5238  isarep1  5407  rexrn  5772  ralrn  5773  elrnrexdmb  5775  fnasrn  5813  fnasrng  5815  foima2  5875  rexima  5878  ralima  5879  abrexco  5883  imaiun  5884  fliftcnv  5919  abrexex2g  6265  abrexex2  6269  tfr1onlemaccex  6494  tfrcllemaccex  6507  tfrcldm  6509  qsid  6747  eroveu  6773  ixp0  6878  infmoti  7195  eldju  7235  ficardon  7361  genpdflem  7694  genpassl  7711  genpassu  7712  nqprm  7729  nqprrnd  7730  ltnqpr  7780  ltnqpri  7781  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemopu  7790  caucvgprprlemaddq  7895  caucvgprprlem1  7896  suplocexprlemml  7903  suplocexprlemloc  7908  caucvgsrlemgt1  7982  elreal  8015  axcaucvglemres  8086  axpre-suploc  8089  dfinfre  9103  suprzclex  9545  supinfneg  9790  infsupneg  9791  ublbneg  9808  4fvwrd4  10336  infssuzex  10453  caucvgre  11492  rexanuz  11499  rexfiuz  11500  resqrexlemglsq  11533  resqrexlemsqa  11535  resqrexlemex  11536  rersqreu  11539  clim0  11796  cbvsum  11871  fsum3  11898  mertenslem2  12047  cbvprod  12069  fprodseq  12094  divalgb  12436  bezoutlemmain  12519  bezoutlemex  12522  pythagtriplem2  12789  pythagtriplem19  12805  pythagtrip  12806  pceu  12818  ennnfoneleminc  12982  ennnfonelemex  12985  ennnfonelemr  12994  imasaddfnlemg  13347  tgval2  14725  ntreq0  14806  metrest  15180  plyun0  15410