Theorem rexbii 2445

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

Syntax hints:   <-> wb 104   T. wtru 1333   E.wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-rex 2423

This theorem is referenced by:  2rexbii  2447  r19.29r  2573  r19.42v  2591  rexcom13  2599  rexrot4  2600  3reeanv  2604  cbvrex2v  2669  rexcom4  2712  rexcom4a  2713  rexcom4b  2714  ceqsrex2v  2821  reu7  2883  0el  3390  iuncom  3827  iuncom4  3828  iuniin  3831  dfiunv2  3857  iunab  3867  iunin2  3884  iundif2ss  3886  iunun  3899  iunxiun  3902  iunpwss  3912  inuni  4088  iunopab  4211  sucel  4340  iunpw  4409  xpiundi  4605  xpiundir  4606  reliin  4669  rexxpf  4694  iunxpf  4695  cnvuni  4733  dmiun  4756  dfima3  4892  rniun  4957  dminxp  4991  imaco  5052  coiun  5056  isarep1  5217  rexrn  5565  ralrn  5566  elrnrexdmb  5568  fnasrn  5606  fnasrng  5608  foima2  5661  rexima  5664  ralima  5665  abrexco  5668  imaiun  5669  fliftcnv  5704  abrexex2g  6026  abrexex2  6030  tfr1onlemaccex  6253  tfrcllemaccex  6266  tfrcldm  6268  qsid  6502  eroveu  6528  ixp0  6633  infmoti  6923  eldju  6961  genpdflem  7339  genpassl  7356  genpassu  7357  nqprm  7374  nqprrnd  7375  ltnqpr  7425  ltnqpri  7426  ltexprlemm  7432  ltexprlemopl  7433  ltexprlemopu  7435  caucvgprprlemaddq  7540  caucvgprprlem1  7541  suplocexprlemml  7548  suplocexprlemloc  7553  caucvgsrlemgt1  7627  elreal  7660  axcaucvglemres  7731  axpre-suploc  7734  dfinfre  8738  suprzclex  9173  supinfneg  9417  infsupneg  9418  ublbneg  9432  4fvwrd4  9948  caucvgre  10785  rexanuz  10792  rexfiuz  10793  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  rersqreu  10832  clim0  11086  cbvsum  11161  fsum3  11188  mertenslem2  11337  cbvprod  11359  fprodseq  11384  divalgb  11658  infssuzex  11678  bezoutlemmain  11722  bezoutlemex  11725  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemr  11972  tgval2  12259  ntreq0  12340  metrest  12714