Theorem rexbii 2515

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 2509	. 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 2487

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-rex 2492

This theorem is referenced by:  2rexbii  2517  r19.29r  2646  r19.42v  2665  rexcom13  2674  rexrot4  2675  3reeanv  2679  cbvrex2vw  2754  cbvrex2v  2756  rexcom4  2800  rexcom4a  2801  rexcom4b  2802  ceqsrex2v  2912  clel5  2917  reu7  2975  0el  3491  iuncom  3947  iuncom4  3948  iuniin  3951  dfiunv2  3977  iunab  3988  iunin2  4005  iundif2ss  4007  iunun  4020  iunxiun  4023  iunpwss  4033  inuni  4215  iunopab  4346  sucel  4475  iunpw  4545  xpiundi  4751  xpiundir  4752  reliin  4815  rexxpf  4843  iunxpf  4844  cnvuni  4882  dmiun  4906  dfima3  5044  rniun  5112  dminxp  5146  imaco  5207  coiun  5211  isarep1  5379  rexrn  5740  ralrn  5741  elrnrexdmb  5743  fnasrn  5781  fnasrng  5783  foima2  5843  rexima  5846  ralima  5847  abrexco  5851  imaiun  5852  fliftcnv  5887  abrexex2g  6228  abrexex2  6232  tfr1onlemaccex  6457  tfrcllemaccex  6470  tfrcldm  6472  qsid  6710  eroveu  6736  ixp0  6841  infmoti  7156  eldju  7196  ficardon  7322  genpdflem  7655  genpassl  7672  genpassu  7673  nqprm  7690  nqprrnd  7691  ltnqpr  7741  ltnqpri  7742  ltexprlemm  7748  ltexprlemopl  7749  ltexprlemopu  7751  caucvgprprlemaddq  7856  caucvgprprlem1  7857  suplocexprlemml  7864  suplocexprlemloc  7869  caucvgsrlemgt1  7943  elreal  7976  axcaucvglemres  8047  axpre-suploc  8050  dfinfre  9064  suprzclex  9506  supinfneg  9751  infsupneg  9752  ublbneg  9769  4fvwrd4  10297  infssuzex  10413  caucvgre  11407  rexanuz  11414  rexfiuz  11415  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  rersqreu  11454  clim0  11711  cbvsum  11786  fsum3  11813  mertenslem2  11962  cbvprod  11984  fprodseq  12009  divalgb  12351  bezoutlemmain  12434  bezoutlemex  12437  pythagtriplem2  12704  pythagtriplem19  12720  pythagtrip  12721  pceu  12733  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemr  12909  imasaddfnlemg  13261  tgval2  14638  ntreq0  14719  metrest  15093  plyun0  15323