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  2824  rexcom4a  2825  rexcom4b  2826  ceqsrex2v  2936  clel5  2941  reu7  2999  0el  3515  iuncom  3974  iuncom4  3975  iuniin  3978  dfiunv2  4004  iunab  4015  iunin2  4032  iundif2ss  4034  iunun  4047  iunxiun  4050  iunpwss  4060  inuni  4243  iunopab  4374  sucel  4505  iunpw  4575  xpiundi  4782  xpiundir  4783  reliin  4847  rexxpf  4875  iunxpf  4876  cnvuni  4914  dmiun  4938  dfima3  5077  rniun  5145  dminxp  5179  imaco  5240  coiun  5244  isarep1  5413  rexrn  5780  ralrn  5781  elrnrexdmb  5783  fnasrn  5821  fnasrng  5823  foima2  5887  rexima  5890  ralima  5891  abrexco  5895  imaiun  5896  fliftcnv  5931  abrexex2g  6277  abrexex2  6281  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfrcldm  6524  qsid  6764  eroveu  6790  ixp0  6895  infmoti  7218  eldju  7258  ficardon  7384  genpdflem  7717  genpassl  7734  genpassu  7735  nqprm  7752  nqprrnd  7753  ltnqpr  7803  ltnqpri  7804  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  caucvgprprlemaddq  7918  caucvgprprlem1  7919  suplocexprlemml  7926  suplocexprlemloc  7931  caucvgsrlemgt1  8005  elreal  8038  axcaucvglemres  8109  axpre-suploc  8112  dfinfre  9126  suprzclex  9568  supinfneg  9819  infsupneg  9820  ublbneg  9837  4fvwrd4  10365  infssuzex  10483  caucvgre  11532  rexanuz  11539  rexfiuz  11540  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  rersqreu  11579  clim0  11836  cbvsum  11911  fsum3  11938  mertenslem2  12087  cbvprod  12109  fprodseq  12134  divalgb  12476  bezoutlemmain  12559  bezoutlemex  12562  pythagtriplem2  12829  pythagtriplem19  12845  pythagtrip  12846  pceu  12858  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemr  13034  imasaddfnlemg  13387  tgval2  14765  ntreq0  14846  metrest  15220  plyun0  15450  clwwlknun  16236