Theorem rexbii 2484

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

Syntax hints:   <-> wb 105   T. wtru 1354   E.wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-rex 2461

This theorem is referenced by:  2rexbii  2486  r19.29r  2615  r19.42v  2634  rexcom13  2642  rexrot4  2643  3reeanv  2647  cbvrex2vw  2715  cbvrex2v  2717  rexcom4  2760  rexcom4a  2761  rexcom4b  2762  ceqsrex2v  2869  clel5  2874  reu7  2932  0el  3445  iuncom  3892  iuncom4  3893  iuniin  3896  dfiunv2  3922  iunab  3933  iunin2  3950  iundif2ss  3952  iunun  3965  iunxiun  3968  iunpwss  3978  inuni  4155  iunopab  4281  sucel  4410  iunpw  4480  xpiundi  4684  xpiundir  4685  reliin  4748  rexxpf  4774  iunxpf  4775  cnvuni  4813  dmiun  4836  dfima3  4973  rniun  5039  dminxp  5073  imaco  5134  coiun  5138  isarep1  5302  rexrn  5653  ralrn  5654  elrnrexdmb  5656  fnasrn  5694  fnasrng  5696  foima2  5752  rexima  5755  ralima  5756  abrexco  5759  imaiun  5760  fliftcnv  5795  abrexex2g  6120  abrexex2  6124  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfrcldm  6363  qsid  6599  eroveu  6625  ixp0  6730  infmoti  7026  eldju  7066  genpdflem  7505  genpassl  7522  genpassu  7523  nqprm  7540  nqprrnd  7541  ltnqpr  7591  ltnqpri  7592  ltexprlemm  7598  ltexprlemopl  7599  ltexprlemopu  7601  caucvgprprlemaddq  7706  caucvgprprlem1  7707  suplocexprlemml  7714  suplocexprlemloc  7719  caucvgsrlemgt1  7793  elreal  7826  axcaucvglemres  7897  axpre-suploc  7900  dfinfre  8912  suprzclex  9350  supinfneg  9594  infsupneg  9595  ublbneg  9612  4fvwrd4  10139  caucvgre  10989  rexanuz  10996  rexfiuz  10997  resqrexlemglsq  11030  resqrexlemsqa  11032  resqrexlemex  11033  rersqreu  11036  clim0  11292  cbvsum  11367  fsum3  11394  mertenslem2  11543  cbvprod  11565  fprodseq  11590  divalgb  11929  infssuzex  11949  bezoutlemmain  11998  bezoutlemex  12001  pythagtriplem2  12265  pythagtriplem19  12281  pythagtrip  12282  pceu  12294  ennnfoneleminc  12411  ennnfonelemex  12414  ennnfonelemr  12423  imasaddfnlemg  12734  tgval2  13521  ntreq0  13602  metrest  13976