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  5774  ralrn  5775  elrnrexdmb  5777  fnasrn  5815  fnasrng  5817  foima2  5881  rexima  5884  ralima  5885  abrexco  5889  imaiun  5890  fliftcnv  5925  abrexex2g  6271  abrexex2  6275  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfrcldm  6515  qsid  6755  eroveu  6781  ixp0  6886  infmoti  7206  eldju  7246  ficardon  7372  genpdflem  7705  genpassl  7722  genpassu  7723  nqprm  7740  nqprrnd  7741  ltnqpr  7791  ltnqpri  7792  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemopu  7801  caucvgprprlemaddq  7906  caucvgprprlem1  7907  suplocexprlemml  7914  suplocexprlemloc  7919  caucvgsrlemgt1  7993  elreal  8026  axcaucvglemres  8097  axpre-suploc  8100  dfinfre  9114  suprzclex  9556  supinfneg  9802  infsupneg  9803  ublbneg  9820  4fvwrd4  10348  infssuzex  10465  caucvgre  11507  rexanuz  11514  rexfiuz  11515  resqrexlemglsq  11548  resqrexlemsqa  11550  resqrexlemex  11551  rersqreu  11554  clim0  11811  cbvsum  11886  fsum3  11913  mertenslem2  12062  cbvprod  12084  fprodseq  12109  divalgb  12451  bezoutlemmain  12534  bezoutlemex  12537  pythagtriplem2  12804  pythagtriplem19  12820  pythagtrip  12821  pceu  12833  ennnfoneleminc  12997  ennnfonelemex  13000  ennnfonelemr  13009  imasaddfnlemg  13362  tgval2  14740  ntreq0  14821  metrest  15195  plyun0  15425