Theorem rexbii 2540

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

Syntax hints:   <-> wb 105   T. wtru 1399   E.wrex 2512

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-rex 2517

This theorem is referenced by:  2rexbii  2542  r19.29r  2672  r19.42v  2691  rexcom13  2700  rexrot4  2701  3reeanv  2705  cbvrex2vw  2780  cbvrex2v  2782  rexcom4  2827  rexcom4a  2828  rexcom4b  2829  ceqsrex2v  2939  clel5  2944  reu7  3002  0el  3519  iuncom  3981  iuncom4  3982  iuniin  3985  dfiunv2  4011  iunab  4022  iunin2  4039  iundif2ss  4041  iunun  4054  iunxiun  4057  iunpwss  4067  inuni  4250  iunopab  4382  sucel  4513  iunpw  4583  xpiundi  4790  xpiundir  4791  reliin  4855  rexxpf  4883  iunxpf  4884  cnvuni  4922  dmiun  4946  dfima3  5085  rniun  5154  dminxp  5188  imaco  5249  coiun  5253  isarep1  5423  rexrn  5792  ralrn  5793  elrnrexdmb  5795  fnasrn  5834  fnasrng  5836  foima2  5902  rexima  5905  ralima  5906  abrexco  5910  imaiun  5911  fliftcnv  5946  abrexex2g  6291  abrexex2  6295  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcldm  6572  qsid  6812  eroveu  6838  ixp0  6943  infmoti  7270  eldju  7310  ficardon  7436  genpdflem  7770  genpassl  7787  genpassu  7788  nqprm  7805  nqprrnd  7806  ltnqpr  7856  ltnqpri  7857  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  caucvgprprlemaddq  7971  caucvgprprlem1  7972  suplocexprlemml  7979  suplocexprlemloc  7984  caucvgsrlemgt1  8058  elreal  8091  axcaucvglemres  8162  axpre-suploc  8165  dfinfre  9178  suprzclex  9622  supinfneg  9873  infsupneg  9874  ublbneg  9891  4fvwrd4  10420  infssuzex  10539  caucvgre  11604  rexanuz  11611  rexfiuz  11612  resqrexlemglsq  11645  resqrexlemsqa  11647  resqrexlemex  11648  rersqreu  11651  clim0  11908  cbvsum  11983  fsum3  12011  mertenslem2  12160  cbvprod  12182  fprodseq  12207  divalgb  12549  bezoutlemmain  12632  bezoutlemex  12635  pythagtriplem2  12902  pythagtriplem19  12918  pythagtrip  12919  pceu  12931  ennnfoneleminc  13095  ennnfonelemex  13098  ennnfonelemr  13107  imasaddfnlemg  13460  tgval2  14845  ntreq0  14926  metrest  15300  plyun0  15530  clwwlknun  16365