Theorem rexbii 2512

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

Syntax hints:   <-> wb 105   T. wtru 1373   E.wrex 2484

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-rex 2489

This theorem is referenced by:  2rexbii  2514  r19.29r  2643  r19.42v  2662  rexcom13  2671  rexrot4  2672  3reeanv  2676  cbvrex2vw  2749  cbvrex2v  2751  rexcom4  2794  rexcom4a  2795  rexcom4b  2796  ceqsrex2v  2904  clel5  2909  reu7  2967  0el  3482  iuncom  3932  iuncom4  3933  iuniin  3936  dfiunv2  3962  iunab  3973  iunin2  3990  iundif2ss  3992  iunun  4005  iunxiun  4008  iunpwss  4018  inuni  4198  iunopab  4327  sucel  4456  iunpw  4526  xpiundi  4732  xpiundir  4733  reliin  4796  rexxpf  4824  iunxpf  4825  cnvuni  4863  dmiun  4886  dfima3  5024  rniun  5092  dminxp  5126  imaco  5187  coiun  5191  isarep1  5359  rexrn  5716  ralrn  5717  elrnrexdmb  5719  fnasrn  5757  fnasrng  5759  foima2  5819  rexima  5822  ralima  5823  abrexco  5827  imaiun  5828  fliftcnv  5863  abrexex2g  6204  abrexex2  6208  tfr1onlemaccex  6433  tfrcllemaccex  6446  tfrcldm  6448  qsid  6686  eroveu  6712  ixp0  6817  infmoti  7129  eldju  7169  ficardon  7295  genpdflem  7619  genpassl  7636  genpassu  7637  nqprm  7654  nqprrnd  7655  ltnqpr  7705  ltnqpri  7706  ltexprlemm  7712  ltexprlemopl  7713  ltexprlemopu  7715  caucvgprprlemaddq  7820  caucvgprprlem1  7821  suplocexprlemml  7828  suplocexprlemloc  7833  caucvgsrlemgt1  7907  elreal  7940  axcaucvglemres  8011  axpre-suploc  8014  dfinfre  9028  suprzclex  9470  supinfneg  9715  infsupneg  9716  ublbneg  9733  4fvwrd4  10261  infssuzex  10374  caucvgre  11263  rexanuz  11270  rexfiuz  11271  resqrexlemglsq  11304  resqrexlemsqa  11306  resqrexlemex  11307  rersqreu  11310  clim0  11567  cbvsum  11642  fsum3  11669  mertenslem2  11818  cbvprod  11840  fprodseq  11865  divalgb  12207  bezoutlemmain  12290  bezoutlemex  12293  pythagtriplem2  12560  pythagtriplem19  12576  pythagtrip  12577  pceu  12589  ennnfoneleminc  12753  ennnfonelemex  12756  ennnfonelemr  12765  imasaddfnlemg  13117  tgval2  14494  ntreq0  14575  metrest  14949  plyun0  15179