Theorem rexbii 2482

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 2476	. 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 2454

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 1445  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-rex 2459

This theorem is referenced by:  2rexbii  2484  r19.29r  2613  r19.42v  2632  rexcom13  2640  rexrot4  2641  3reeanv  2645  cbvrex2vw  2713  cbvrex2v  2715  rexcom4  2758  rexcom4a  2759  rexcom4b  2760  ceqsrex2v  2867  clel5  2872  reu7  2930  0el  3443  iuncom  3888  iuncom4  3889  iuniin  3892  dfiunv2  3918  iunab  3928  iunin2  3945  iundif2ss  3947  iunun  3960  iunxiun  3963  iunpwss  3973  inuni  4150  iunopab  4275  sucel  4404  iunpw  4474  xpiundi  4678  xpiundir  4679  reliin  4742  rexxpf  4767  iunxpf  4768  cnvuni  4806  dmiun  4829  dfima3  4966  rniun  5031  dminxp  5065  imaco  5126  coiun  5130  isarep1  5294  rexrn  5645  ralrn  5646  elrnrexdmb  5648  fnasrn  5686  fnasrng  5688  foima2  5743  rexima  5746  ralima  5747  abrexco  5750  imaiun  5751  fliftcnv  5786  abrexex2g  6111  abrexex2  6115  tfr1onlemaccex  6339  tfrcllemaccex  6352  tfrcldm  6354  qsid  6590  eroveu  6616  ixp0  6721  infmoti  7017  eldju  7057  genpdflem  7481  genpassl  7498  genpassu  7499  nqprm  7516  nqprrnd  7517  ltnqpr  7567  ltnqpri  7568  ltexprlemm  7574  ltexprlemopl  7575  ltexprlemopu  7577  caucvgprprlemaddq  7682  caucvgprprlem1  7683  suplocexprlemml  7690  suplocexprlemloc  7695  caucvgsrlemgt1  7769  elreal  7802  axcaucvglemres  7873  axpre-suploc  7876  dfinfre  8886  suprzclex  9324  supinfneg  9568  infsupneg  9569  ublbneg  9586  4fvwrd4  10110  caucvgre  10958  rexanuz  10965  rexfiuz  10966  resqrexlemglsq  10999  resqrexlemsqa  11001  resqrexlemex  11002  rersqreu  11005  clim0  11261  cbvsum  11336  fsum3  11363  mertenslem2  11512  cbvprod  11534  fprodseq  11559  divalgb  11897  infssuzex  11917  bezoutlemmain  11966  bezoutlemex  11969  pythagtriplem2  12233  pythagtriplem19  12249  pythagtrip  12250  pceu  12262  ennnfoneleminc  12379  ennnfonelemex  12382  ennnfonelemr  12391  tgval2  13131  ntreq0  13212  metrest  13586