Theorem rexbii 2501

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 2495	. 2 |- ( T. -> ( E. x e. A ph <-> E. x e. A ps ) )
4	3	mptru 1373	1 |- ( E. x e. A ph <-> E. x e. A ps )

Syntax hints:   <-> wb 105   T. wtru 1365   E.wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-rex 2478

This theorem is referenced by:  2rexbii  2503  r19.29r  2632  r19.42v  2651  rexcom13  2660  rexrot4  2661  3reeanv  2665  cbvrex2vw  2738  cbvrex2v  2740  rexcom4  2783  rexcom4a  2784  rexcom4b  2785  ceqsrex2v  2892  clel5  2897  reu7  2955  0el  3469  iuncom  3918  iuncom4  3919  iuniin  3922  dfiunv2  3948  iunab  3959  iunin2  3976  iundif2ss  3978  iunun  3991  iunxiun  3994  iunpwss  4004  inuni  4184  iunopab  4312  sucel  4441  iunpw  4511  xpiundi  4717  xpiundir  4718  reliin  4781  rexxpf  4809  iunxpf  4810  cnvuni  4848  dmiun  4871  dfima3  5008  rniun  5076  dminxp  5110  imaco  5171  coiun  5175  isarep1  5340  rexrn  5695  ralrn  5696  elrnrexdmb  5698  fnasrn  5736  fnasrng  5738  foima2  5794  rexima  5797  ralima  5798  abrexco  5802  imaiun  5803  fliftcnv  5838  abrexex2g  6172  abrexex2  6176  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfrcldm  6416  qsid  6654  eroveu  6680  ixp0  6785  infmoti  7087  eldju  7127  genpdflem  7567  genpassl  7584  genpassu  7585  nqprm  7602  nqprrnd  7603  ltnqpr  7653  ltnqpri  7654  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  caucvgprprlemaddq  7768  caucvgprprlem1  7769  suplocexprlemml  7776  suplocexprlemloc  7781  caucvgsrlemgt1  7855  elreal  7888  axcaucvglemres  7959  axpre-suploc  7962  dfinfre  8975  suprzclex  9415  supinfneg  9660  infsupneg  9661  ublbneg  9678  4fvwrd4  10206  caucvgre  11125  rexanuz  11132  rexfiuz  11133  resqrexlemglsq  11166  resqrexlemsqa  11168  resqrexlemex  11169  rersqreu  11172  clim0  11428  cbvsum  11503  fsum3  11530  mertenslem2  11679  cbvprod  11701  fprodseq  11726  divalgb  12066  infssuzex  12086  bezoutlemmain  12135  bezoutlemex  12138  pythagtriplem2  12404  pythagtriplem19  12420  pythagtrip  12421  pceu  12433  ennnfoneleminc  12568  ennnfonelemex  12571  ennnfonelemr  12580  imasaddfnlemg  12897  tgval2  14219  ntreq0  14300  metrest  14674  plyun0  14882