Theorem rexbii 2373

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 2369	. 2 |- ( T. -> ( E. x e. A ph <-> E. x e. A ps ) )
4	3	trud 1293	1 |- ( E. x e. A ph <-> E. x e. A ps )

Syntax hints:   <-> wb 103   T. wtru 1285   E.wrex 2349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-rex 2354

This theorem is referenced by:  2rexbii  2375  r19.29r  2495  r19.42v  2511  rexcom13  2519  rexrot4  2520  3reeanv  2524  cbvrex2v  2586  rexcom4  2622  rexcom4a  2623  rexcom4b  2624  ceqsrex2v  2727  reu7  2787  0el  3268  iuncom  3684  iuncom4  3685  iuniin  3688  dfiunv2  3714  iunab  3724  iunin2  3741  iundif2ss  3743  iunun  3755  iunxiun  3757  iunpwss  3764  inuni  3930  iunopab  4036  sucel  4165  iunpw  4229  xpiundi  4416  xpiundir  4417  reliin  4477  rexxpf  4501  iunxpf  4502  cnvuni  4539  dmiun  4562  dfima3  4691  rniun  4754  dminxp  4785  imaco  4846  coiun  4850  isarep1  5005  rexrn  5325  ralrn  5326  elrnrexdmb  5328  fnasrn  5362  fnasrng  5364  rexima  5415  ralima  5416  abrexco  5419  imaiun  5420  fliftcnv  5455  abrexex2g  5767  abrexex2  5771  qsid  6194  eroveu  6220  infmoti  6441  genpdflem  6697  genpassl  6714  genpassu  6715  nqprm  6732  nqprrnd  6733  ltnqpr  6783  ltnqpri  6784  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgsrlemgt1  6971  elreal  6997  axcaucvglemres  7065  dfinfre  8034  suprzclex  8445  supinfneg  8683  infsupneg  8684  ublbneg  8698  4fvwrd4  9150  caucvgre  9867  rexanuz  9874  rexfiuz  9875  resqrexlemglsq  9908  resqrexlemsqa  9910  resqrexlemex  9911  rersqreu  9914  clim0  10124  divalgb  10325  infssuzex  10345  bezoutlemmain  10387  bezoutlemex  10390