Theorem exbii 1496

Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)

Hypothesis

Ref	Expression
exbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
exbii	|- ( E. x ph <-> E. x ps )

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1495	. 2 |- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2		exbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1340	1 |- ( E. x ph <-> E. x ps )

Syntax hints:   <-> wb 98   E.wex 1381

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-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2exbii  1497  3exbii  1498  exancom  1499  excom13  1579  exrot4  1581  eeor  1585  sbcof2  1691  sbequ8  1727  sbidm  1731  sborv  1770  19.41vv  1783  19.41vvv  1784  19.41vvvv  1785  exdistr  1787  19.42vvv  1789  exdistr2  1791  3exdistr  1792  4exdistr  1793  eean  1806  eeeanv  1808  ee4anv  1809  2sb5  1859  2sb5rf  1865  sbel2x  1874  sbexyz  1879  sbex  1880  exsb  1884  2exsb  1885  sb8eu  1913  sb8euh  1923  eu1  1925  eu2  1944  2moswapdc  1990  2exeu  1992  exists1  1996  clelab  2162  clabel  2163  sbabel  2203  rexbii2  2335  r2exf  2342  nfrexdya  2359  r19.41  2465  r19.43  2468  isset  2561  rexv  2572  ceqsex2  2594  ceqsex3v  2596  gencbvex  2600  ceqsrexv  2674  rexab  2703  rexrab2  2708  euxfrdc  2727  euind  2728  reu6  2730  reu3  2731  2reuswapdc  2743  reuind  2744  sbccomlem  2832  rmo2ilem  2847  rexun  3123  reupick3  3222  abn0r  3243  rabn0m  3245  rexsns  3409  rexsnsOLD  3410  exsnrex  3413  snprc  3435  euabsn2  3439  reusn  3441  eusn  3444  elunirab  3593  unipr  3594  uniun  3599  uniin  3600  iuncom4  3664  dfiun2g  3689  iunn0m  3717  iunxiun  3736  cbvopab2  3831  cbvopab2v  3834  unopab  3836  zfnuleu  3881  0ex  3884  vprc  3888  inex1  3891  intexabim  3906  iinexgm  3908  inuni  3909  unidif0  3920  axpweq  3924  zfpow  3928  axpow2  3929  axpow3  3930  pwex  3932  zfpair2  3945  mss  3962  exss  3963  opm  3971  eqvinop  3980  copsexg  3981  opabm  4017  iunopab  4018  zfun  4171  uniex2  4173  uniuni  4183  rexxfrd  4195  dtruex  4283  zfinf2  4312  elxp2  4363  opeliunxp  4395  xpiundi  4398  xpiundir  4399  elvvv  4403  eliunxp  4475  rexiunxp  4478  relop  4486  opelco2g  4503  cnvco  4520  cnvuni  4521  dfdm3  4522  dfrn2  4523  dfrn3  4524  elrng  4526  dfdm4  4527  eldm2g  4531  dmun  4542  dmin  4543  dmiun  4544  dmuni  4545  dmopab  4546  dmi  4550  dmmrnm  4554  elrn  4577  rnopab  4581  dmcosseq  4603  dmres  4632  elres  4646  elsnres  4647  dfima2  4670  elima3  4675  imadmrn  4678  imai  4681  args  4694  rniun  4734  ssrnres  4763  dmsnm  4786  dmsnopg  4792  elxp4  4808  elxp5  4809  cnvresima  4810  mptpreima  4814  dfco2  4820  coundi  4822  coundir  4823  resco  4825  imaco  4826  rnco  4827  coiun  4830  coi1  4836  coass  4839  xpcom  4864  dffun2  4912  imadif  4979  imainlem  4980  funimaexglem  4982  fun11iun  5147  f11o  5159  brprcneu  5171  nfvres  5206  fndmin  5274  abrexco  5398  imaiun  5399  dfoprab2  5552  cbvoprab2  5577  rexrnmpt2  5616  opabex3d  5748  opabex3  5749  abexssex  5752  abexex  5753  oprabrexex2  5757  releldm2  5811  dfopab2  5815  dfoprab3s  5816  brtpos2  5866  domen  6232  xpsnen  6295  xpcomco  6300  xpassen  6304  subhalfnqq  6512  ltbtwnnq  6514  prnmaxl  6586  prnminu  6587  prarloc  6601  genpdflem  6605  genpassl  6622  genpassu  6623  ltexprlemm  6698  2rexuz  8525  bj-axempty  10013  bj-axempty2  10014  bj-vprc  10016  bdinex1  10019  bj-zfpair2  10030  bj-uniex2  10036  bj-d0clsepcl  10049