Theorem rexbii 2549

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 2543	. 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 2521

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 2526

This theorem is referenced by:  2rexbii  2551  r19.29r  2681  r19.42v  2700  rexcom13  2709  rexrot4  2710  3reeanv  2714  cbvrex2vw  2790  cbvrex2v  2792  rexcom4  2837  rexcom4a  2838  rexcom4b  2839  ceqsrex2v  2949  clel5  2954  reu7  3012  0el  3531  iuncom  3997  iuncom4  3998  iuniin  4001  dfiunv2  4027  iunab  4038  iunin2  4055  iundif2ss  4057  iunun  4070  iunxiun  4073  iunpwss  4083  inuni  4267  iunopab  4400  sucel  4531  iunpw  4601  xpiundi  4808  xpiundir  4809  reliin  4874  rexxpf  4902  iunxpf  4903  cnvuni  4941  dmiun  4965  dfima3  5104  rniun  5173  dminxp  5207  imaco  5268  coiun  5272  isarep1  5442  rexrn  5814  ralrn  5815  elrnrexdmb  5817  fnasrn  5856  fnasrng  5858  foima2  5924  rexima  5927  ralima  5928  abrexco  5932  imaiun  5933  fliftcnv  5968  abrexex2g  6313  abrexex2  6317  tfr1onlemaccex  6579  tfrcllemaccex  6592  tfrcldm  6594  qsid  6834  eroveu  6860  ixp0  6966  infmoti  7319  eldju  7359  ficardon  7485  genpdflem  7822  genpassl  7839  genpassu  7840  nqprm  7857  nqprrnd  7858  ltnqpr  7908  ltnqpri  7909  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  caucvgprprlemaddq  8023  caucvgprprlem1  8024  suplocexprlemml  8031  suplocexprlemloc  8036  caucvgsrlemgt1  8110  elreal  8143  axcaucvglemres  8214  axpre-suploc  8217  dfinfre  9230  suprzclex  9676  supinfneg  9927  infsupneg  9928  ublbneg  9945  4fvwrd4  10474  infssuzex  10593  caucvgre  11666  rexanuz  11673  rexfiuz  11674  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  rersqreu  11713  clim0  11970  cbvsum  12045  fsum3  12073  mertenslem2  12222  cbvprod  12244  fprodseq  12269  divalgb  12611  bezoutlemmain  12694  bezoutlemex  12697  pythagtriplem2  12964  pythagtriplem19  12980  pythagtrip  12981  pceu  12993  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemr  13174  imasaddfnlemg  13527  tgval2  14916  ntreq0  14997  metrest  15371  plyun0  15601  clwwlknun  16436