Theorem rexbii 2331

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

Syntax hints:   <-> wb 98   T. wtru 1244   E.wrex 2307

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-rex 2312

This theorem is referenced by:  2rexbii  2333  r19.29r  2451  r19.42v  2467  rexcom13  2475  rexrot4  2476  3reeanv  2480  cbvrex2v  2542  rexcom4  2577  rexcom4a  2578  rexcom4b  2579  ceqsrex2v  2676  reu7  2736  0el  3241  iuncom  3663  iuncom4  3664  iuniin  3667  dfiunv2  3693  iunab  3703  iunin2  3720  iundif2ss  3722  iunun  3734  iunxiun  3736  iunpwss  3743  inuni  3909  iunopab  4018  sucel  4147  iunpw  4211  xpiundi  4398  xpiundir  4399  reliin  4459  rexxpf  4483  iunxpf  4484  cnvuni  4521  dmiun  4544  dfima3  4671  rniun  4734  dminxp  4765  imaco  4826  coiun  4830  isarep1  4985  rexrn  5304  ralrn  5305  elrnrexdmb  5307  fnasrn  5341  fnasrng  5343  rexima  5394  ralima  5395  abrexco  5398  imaiun  5399  fliftcnv  5435  abrexex2g  5747  abrexex2  5751  qsid  6171  eroveu  6197  genpdflem  6605  genpassl  6622  genpassu  6623  nqprm  6640  nqprrnd  6641  ltnqpr  6691  ltnqpri  6692  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  caucvgprprlemaddq  6806  caucvgprprlem1  6807  caucvgsrlemgt1  6879  elreal  6905  axcaucvglemres  6973  ublbneg  8548  4fvwrd4  8997  caucvgre  9580  rexanuz  9587  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  rersqreu  9626  clim0  9806