Theorem rexbii 2513

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

Syntax hints:   <-> wb 105   T. wtru 1374   E.wrex 2485

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-rex 2490

This theorem is referenced by:  2rexbii  2515  r19.29r  2644  r19.42v  2663  rexcom13  2672  rexrot4  2673  3reeanv  2677  cbvrex2vw  2750  cbvrex2v  2752  rexcom4  2795  rexcom4a  2796  rexcom4b  2797  ceqsrex2v  2905  clel5  2910  reu7  2968  0el  3483  iuncom  3933  iuncom4  3934  iuniin  3937  dfiunv2  3963  iunab  3974  iunin2  3991  iundif2ss  3993  iunun  4006  iunxiun  4009  iunpwss  4019  inuni  4199  iunopab  4328  sucel  4457  iunpw  4527  xpiundi  4733  xpiundir  4734  reliin  4797  rexxpf  4825  iunxpf  4826  cnvuni  4864  dmiun  4887  dfima3  5025  rniun  5093  dminxp  5127  imaco  5188  coiun  5192  isarep1  5360  rexrn  5717  ralrn  5718  elrnrexdmb  5720  fnasrn  5758  fnasrng  5760  foima2  5820  rexima  5823  ralima  5824  abrexco  5828  imaiun  5829  fliftcnv  5864  abrexex2g  6205  abrexex2  6209  tfr1onlemaccex  6434  tfrcllemaccex  6447  tfrcldm  6449  qsid  6687  eroveu  6713  ixp0  6818  infmoti  7130  eldju  7170  ficardon  7296  genpdflem  7620  genpassl  7637  genpassu  7638  nqprm  7655  nqprrnd  7656  ltnqpr  7706  ltnqpri  7707  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemopu  7716  caucvgprprlemaddq  7821  caucvgprprlem1  7822  suplocexprlemml  7829  suplocexprlemloc  7834  caucvgsrlemgt1  7908  elreal  7941  axcaucvglemres  8012  axpre-suploc  8015  dfinfre  9029  suprzclex  9471  supinfneg  9716  infsupneg  9717  ublbneg  9734  4fvwrd4  10262  infssuzex  10376  caucvgre  11292  rexanuz  11299  rexfiuz  11300  resqrexlemglsq  11333  resqrexlemsqa  11335  resqrexlemex  11336  rersqreu  11339  clim0  11596  cbvsum  11671  fsum3  11698  mertenslem2  11847  cbvprod  11869  fprodseq  11894  divalgb  12236  bezoutlemmain  12319  bezoutlemex  12322  pythagtriplem2  12589  pythagtriplem19  12605  pythagtrip  12606  pceu  12618  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemr  12794  imasaddfnlemg  13146  tgval2  14523  ntreq0  14604  metrest  14978  plyun0  15208