Theorem rexbii 2539

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

Syntax hints:   <-> wb 105   T. wtru 1398   E.wrex 2511

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-rex 2516

This theorem is referenced by:  2rexbii  2541  r19.29r  2671  r19.42v  2690  rexcom13  2699  rexrot4  2700  3reeanv  2704  cbvrex2vw  2779  cbvrex2v  2781  rexcom4  2826  rexcom4a  2827  rexcom4b  2828  ceqsrex2v  2938  clel5  2943  reu7  3001  0el  3517  iuncom  3976  iuncom4  3977  iuniin  3980  dfiunv2  4006  iunab  4017  iunin2  4034  iundif2ss  4036  iunun  4049  iunxiun  4052  iunpwss  4062  inuni  4245  iunopab  4376  sucel  4507  iunpw  4577  xpiundi  4784  xpiundir  4785  reliin  4849  rexxpf  4877  iunxpf  4878  cnvuni  4916  dmiun  4940  dfima3  5079  rniun  5147  dminxp  5181  imaco  5242  coiun  5246  isarep1  5416  rexrn  5784  ralrn  5785  elrnrexdmb  5787  fnasrn  5825  fnasrng  5827  foima2  5891  rexima  5894  ralima  5895  abrexco  5899  imaiun  5900  fliftcnv  5935  abrexex2g  6281  abrexex2  6285  tfr1onlemaccex  6513  tfrcllemaccex  6526  tfrcldm  6528  qsid  6768  eroveu  6794  ixp0  6899  infmoti  7226  eldju  7266  ficardon  7392  genpdflem  7726  genpassl  7743  genpassu  7744  nqprm  7761  nqprrnd  7762  ltnqpr  7812  ltnqpri  7813  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  caucvgprprlemaddq  7927  caucvgprprlem1  7928  suplocexprlemml  7935  suplocexprlemloc  7940  caucvgsrlemgt1  8014  elreal  8047  axcaucvglemres  8118  axpre-suploc  8121  dfinfre  9135  suprzclex  9577  supinfneg  9828  infsupneg  9829  ublbneg  9846  4fvwrd4  10374  infssuzex  10492  caucvgre  11541  rexanuz  11548  rexfiuz  11549  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  rersqreu  11588  clim0  11845  cbvsum  11920  fsum3  11947  mertenslem2  12096  cbvprod  12118  fprodseq  12143  divalgb  12485  bezoutlemmain  12568  bezoutlemex  12571  pythagtriplem2  12838  pythagtriplem19  12854  pythagtrip  12855  pceu  12867  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemr  13043  imasaddfnlemg  13396  tgval2  14774  ntreq0  14855  metrest  15229  plyun0  15459  clwwlknun  16291