Theorem rexbii 2557

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

Syntax hints:   <-> wb 105   T. wtru 1403   E.wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-rex 2534

This theorem is referenced by:  2rexbii  2559  r19.29r  2689  r19.42v  2708  rexcom13  2717  rexrot4  2718  3reeanv  2722  cbvrex2vw  2798  cbvrex2v  2800  rexcom4  2845  rexcom4a  2846  rexcom4b  2847  ceqsrex2v  2958  clel5  2963  reu7  3021  0el  3544  iuncom  4013  iuncom4  4014  iuniin  4017  dfiunv2  4043  iunab  4054  iunin2  4071  iundif2ss  4073  iunun  4086  iunxiun  4089  iunpwss  4099  inuni  4286  iunopab  4419  sucel  4550  iunpw  4621  xpiundi  4828  xpiundir  4829  reliin  4894  rexxpf  4922  iunxpf  4923  cnvuni  4961  dmiun  4985  dfima3  5124  rniun  5193  dminxp  5227  imaco  5288  coiun  5292  isarep1  5462  rexrn  5836  ralrn  5837  elrnrexdmb  5839  fnasrn  5878  fnasrng  5880  foima2  5947  rexima  5950  ralima  5951  abrexco  5955  imaiun  5956  fliftcnv  5991  abrexex2g  6339  abrexex2  6343  tfr1onlemaccex  6609  tfrcllemaccex  6622  tfrcldm  6624  qsid  6864  eroveu  6890  ixp0  7003  infmoti  7358  eldju  7398  ficardon  7524  genpdflem  7864  genpassl  7881  genpassu  7882  nqprm  7899  nqprrnd  7900  ltnqpr  7950  ltnqpri  7951  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  caucvgprprlemaddq  8065  caucvgprprlem1  8066  suplocexprlemml  8073  suplocexprlemloc  8078  caucvgsrlemgt1  8152  elreal  8185  axcaucvglemres  8256  axpre-suploc  8259  dfinfre  9276  suprzclex  9723  supinfneg  9974  infsupneg  9975  ublbneg  9992  4fvwrd4  10525  infssuzex  10644  caucvgre  11725  rexanuz  11732  rexfiuz  11733  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  rersqreu  11772  clim0  12029  cbvsum  12104  fsum3  12132  mertenslem2  12281  cbvprod  12303  fprodseq  12328  divalgb  12670  bezoutlemmain  12753  bezoutlemex  12756  pythagtriplem2  13023  pythagtriplem19  13039  pythagtrip  13040  pceu  13052  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemr  13292  imasaddfnlemg  13612  tgval2  15075  ntreq0  15156  metrest  15530  plyun0  15760  clwwlknun  16596