Theorem rexbii 2325

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

Syntax hints:   <-> wb 98   T. wtru 1243  E.wrex 2301

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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-rex 2306

This theorem is referenced by:  2rexbii  2327  r19.29r  2445  r19.42v  2461  rexcom13  2469  rexrot4  2470  3reeanv  2474  cbvrex2v  2536  rexcom4  2571  rexcom4a  2572  rexcom4b  2573  ceqsrex2v  2670  reu7  2730  0el  3235  iuncom  3654  iuncom4  3655  iuniin  3658  dfiunv2  3684  iunab  3694  iunin2  3711  iundif2ss  3713  iunun  3725  iunxiun  3727  iunpwss  3734  inuni  3900  iunopab  4009  sucel  4113  iunpw  4177  xpiundi  4341  xpiundir  4342  reliin  4402  rexxpf  4426  iunxpf  4427  cnvuni  4464  dmiun  4487  dfima3  4614  rniun  4677  dminxp  4708  imaco  4769  coiun  4773  isarep1  4928  rexrn  5247  ralrn  5248  elrnrexdmb  5250  fnasrn  5284  fnasrng  5286  rexima  5337  ralima  5338  abrexco  5341  imaiun  5342  fliftcnv  5378  abrexex2g  5689  abrexex2  5693  qsid  6107  eroveu  6133  genpdflem  6489  genpassl  6506  genpassu  6507  nqprm  6524  nqprrnd  6525  ltexprlemm  6573  ltexprlemopl  6574  ltexprlemopu  6576  elreal  6707  ublbneg  8304  4fvwrd4  8747