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  2823  rexcom4a  2824  rexcom4b  2825  ceqsrex2v  2935  clel5  2940  reu7  2998  0el  3514  iuncom  3970  iuncom4  3971  iuniin  3974  dfiunv2  4000  iunab  4011  iunin2  4028  iundif2ss  4030  iunun  4043  iunxiun  4046  iunpwss  4056  inuni  4238  iunopab  4369  sucel  4500  iunpw  4570  xpiundi  4776  xpiundir  4777  reliin  4840  rexxpf  4868  iunxpf  4869  cnvuni  4907  dmiun  4931  dfima3  5070  rniun  5138  dminxp  5172  imaco  5233  coiun  5237  isarep1  5406  rexrn  5771  ralrn  5772  elrnrexdmb  5774  fnasrn  5812  fnasrng  5814  foima2  5874  rexima  5877  ralima  5878  abrexco  5882  imaiun  5883  fliftcnv  5918  abrexex2g  6263  abrexex2  6267  tfr1onlemaccex  6492  tfrcllemaccex  6505  tfrcldm  6507  qsid  6745  eroveu  6771  ixp0  6876  infmoti  7191  eldju  7231  ficardon  7357  genpdflem  7690  genpassl  7707  genpassu  7708  nqprm  7725  nqprrnd  7726  ltnqpr  7776  ltnqpri  7777  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemopu  7786  caucvgprprlemaddq  7891  caucvgprprlem1  7892  suplocexprlemml  7899  suplocexprlemloc  7904  caucvgsrlemgt1  7978  elreal  8011  axcaucvglemres  8082  axpre-suploc  8085  dfinfre  9099  suprzclex  9541  supinfneg  9786  infsupneg  9787  ublbneg  9804  4fvwrd4  10332  infssuzex  10448  caucvgre  11487  rexanuz  11494  rexfiuz  11495  resqrexlemglsq  11528  resqrexlemsqa  11530  resqrexlemex  11531  rersqreu  11534  clim0  11791  cbvsum  11866  fsum3  11893  mertenslem2  12042  cbvprod  12064  fprodseq  12089  divalgb  12431  bezoutlemmain  12514  bezoutlemex  12517  pythagtriplem2  12784  pythagtriplem19  12800  pythagtrip  12801  pceu  12813  ennnfoneleminc  12977  ennnfonelemex  12980  ennnfonelemr  12989  imasaddfnlemg  13342  tgval2  14719  ntreq0  14800  metrest  15174  plyun0  15404