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  2893  clel5  2898  reu7  2956  0el  3470  iuncom  3919  iuncom4  3920  iuniin  3923  dfiunv2  3949  iunab  3960  iunin2  3977  iundif2ss  3979  iunun  3992  iunxiun  3995  iunpwss  4005  inuni  4185  iunopab  4313  sucel  4442  iunpw  4512  xpiundi  4718  xpiundir  4719  reliin  4782  rexxpf  4810  iunxpf  4811  cnvuni  4849  dmiun  4872  dfima3  5009  rniun  5077  dminxp  5111  imaco  5172  coiun  5176  isarep1  5341  rexrn  5696  ralrn  5697  elrnrexdmb  5699  fnasrn  5737  fnasrng  5739  foima2  5795  rexima  5798  ralima  5799  abrexco  5803  imaiun  5804  fliftcnv  5839  abrexex2g  6174  abrexex2  6178  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfrcldm  6418  qsid  6656  eroveu  6682  ixp0  6787  infmoti  7089  eldju  7129  genpdflem  7569  genpassl  7586  genpassu  7587  nqprm  7604  nqprrnd  7605  ltnqpr  7655  ltnqpri  7656  ltexprlemm  7662  ltexprlemopl  7663  ltexprlemopu  7665  caucvgprprlemaddq  7770  caucvgprprlem1  7771  suplocexprlemml  7778  suplocexprlemloc  7783  caucvgsrlemgt1  7857  elreal  7890  axcaucvglemres  7961  axpre-suploc  7964  dfinfre  8977  suprzclex  9418  supinfneg  9663  infsupneg  9664  ublbneg  9681  4fvwrd4  10209  caucvgre  11128  rexanuz  11135  rexfiuz  11136  resqrexlemglsq  11169  resqrexlemsqa  11171  resqrexlemex  11172  rersqreu  11175  clim0  11431  cbvsum  11506  fsum3  11533  mertenslem2  11682  cbvprod  11704  fprodseq  11729  divalgb  12069  infssuzex  12089  bezoutlemmain  12138  bezoutlemex  12141  pythagtriplem2  12407  pythagtriplem19  12423  pythagtrip  12424  pceu  12436  ennnfoneleminc  12571  ennnfonelemex  12574  ennnfonelemr  12583  imasaddfnlemg  12900  tgval2  14230  ntreq0  14311  metrest  14685  plyun0  14915