Theorem rexbii 2386

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

Syntax hints:   <-> wb 104   T. wtru 1291   E.wrex 2361

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-rex 2366

This theorem is referenced by:  2rexbii  2388  r19.29r  2508  r19.42v  2525  rexcom13  2533  rexrot4  2534  3reeanv  2538  cbvrex2v  2600  rexcom4  2643  rexcom4a  2644  rexcom4b  2645  ceqsrex2v  2750  reu7  2811  0el  3309  iuncom  3742  iuncom4  3743  iuniin  3746  dfiunv2  3772  iunab  3782  iunin2  3799  iundif2ss  3801  iunun  3814  iunxiun  3816  iunpwss  3826  inuni  3997  iunopab  4117  sucel  4246  iunpw  4315  xpiundi  4509  xpiundir  4510  reliin  4572  rexxpf  4596  iunxpf  4597  cnvuni  4635  dmiun  4658  dfima3  4790  rniun  4855  dminxp  4888  imaco  4949  coiun  4953  isarep1  5113  rexrn  5450  ralrn  5451  elrnrexdmb  5453  fnasrn  5489  fnasrng  5491  foima2  5544  rexima  5548  ralima  5549  abrexco  5552  imaiun  5553  fliftcnv  5588  abrexex2g  5905  abrexex2  5909  tfr1onlemaccex  6127  tfrcllemaccex  6140  tfrcldm  6142  qsid  6371  eroveu  6397  ixp0  6502  infmoti  6777  eldju  6813  genpdflem  7127  genpassl  7144  genpassu  7145  nqprm  7162  nqprrnd  7163  ltnqpr  7213  ltnqpri  7214  ltexprlemm  7220  ltexprlemopl  7221  ltexprlemopu  7223  caucvgprprlemaddq  7328  caucvgprprlem1  7329  caucvgsrlemgt1  7401  elreal  7427  axcaucvglemres  7495  dfinfre  8478  suprzclex  8905  supinfneg  9144  infsupneg  9145  ublbneg  9159  4fvwrd4  9612  caucvgre  10475  rexanuz  10482  rexfiuz  10483  resqrexlemglsq  10516  resqrexlemsqa  10518  resqrexlemex  10519  rersqreu  10522  clim0  10734  cbvsum  10810  fisum  10839  mertenslem2  10991  divalgb  11264  infssuzex  11284  bezoutlemmain  11326  bezoutlemex  11329  tgval2  11812  ntreq0  11893