Theorem exbii 1598

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 1597	. 2 |- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2		exbii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1444	1 |- ( E. x ph <-> E. x ps )

Syntax hints:   <-> wb 104   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1599  3exbii  1600  exancom  1601  excom13  1682  exrot4  1684  eeor  1688  sbcof2  1803  sbequ8  1840  sbidm  1844  sborv  1883  19.41vv  1896  19.41vvv  1897  19.41vvvv  1898  exdistr  1902  19.42vvv  1905  exdistr2  1907  3exdistr  1908  4exdistr  1909  eean  1924  eeeanv  1926  ee4anv  1927  2sb5  1976  2sb5rf  1982  sbel2x  1991  sbexyz  1996  sbex  1997  exsb  2001  2exsb  2002  sb8eu  2032  sb8euh  2042  eu1  2044  eu2  2063  2moswapdc  2109  2exeu  2111  exists1  2115  clelab  2296  clabel  2297  sbabel  2339  rexbii2  2481  r2exf  2488  nfrexdya  2506  r19.41  2625  r19.43  2628  cbvreuvw  2702  isset  2736  rexv  2748  ceqsex2  2770  ceqsex3v  2772  gencbvex  2776  ceqsrexv  2860  rexab  2892  rexrab2  2897  euxfrdc  2916  euind  2917  reu6  2919  reu3  2920  2reuswapdc  2934  reuind  2935  sbccomlem  3029  rmo2ilem  3044  rexun  3307  reupick3  3412  abn0r  3439  abn0m  3440  rabn0m  3442  rexsns  3622  exsnrex  3625  snprc  3648  euabsn2  3652  reusn  3654  eusn  3657  elunirab  3809  unipr  3810  uniun  3815  uniin  3816  iuncom4  3880  dfiun2g  3905  iunn0m  3933  iunxiun  3954  disjnim  3980  cbvopab2  4063  cbvopab2v  4066  unopab  4068  zfnuleu  4113  0ex  4116  vnex  4120  inex1  4123  intexabim  4138  iinexgm  4140  inuni  4141  unidif0  4153  axpweq  4157  zfpow  4161  axpow2  4162  axpow3  4163  vpwex  4165  zfpair2  4195  mss  4211  exss  4212  opm  4219  eqvinop  4228  copsexg  4229  opabm  4265  iunopab  4266  zfun  4419  uniex2  4421  uniuni  4436  rexxfrd  4448  dtruex  4543  zfinf2  4573  elxp2  4629  opeliunxp  4666  xpiundi  4669  xpiundir  4670  elvvv  4674  eliunxp  4750  rexiunxp  4753  relop  4761  elco  4777  opelco2g  4779  cnvco  4796  cnvuni  4797  dfdm3  4798  dfrn2  4799  dfrn3  4800  elrng  4802  dfdm4  4803  eldm2g  4807  dmun  4818  dmin  4819  dmiun  4820  dmuni  4821  dmopab  4822  dmi  4826  dmmrnm  4830  elrn  4854  rnopab  4858  dmcosseq  4882  dmres  4912  elres  4927  elsnres  4928  dfima2  4955  elima3  4960  imadmrn  4963  imai  4967  args  4980  rniun  5021  ssrnres  5053  dmsnm  5076  dmsnopg  5082  elxp4  5098  elxp5  5099  cnvresima  5100  mptpreima  5104  dfco2  5110  coundi  5112  coundir  5113  resco  5115  imaco  5116  rnco  5117  coiun  5120  coi1  5126  coass  5129  xpcom  5157  dffun2  5208  imadif  5278  imainlem  5279  funimaexglem  5281  fun11iun  5463  f11o  5475  brprcneu  5489  nfvres  5529  fndmin  5603  abrexco  5738  imaiun  5739  dfoprab2  5900  cbvoprab2  5926  rexrnmpo  5968  opabex3d  6100  opabex3  6101  abexssex  6104  abexex  6105  oprabrexex2  6109  releldm2  6164  dfopab2  6168  dfoprab3s  6169  cnvoprab  6213  brtpos2  6230  tfr1onlemaccex  6327  tfrcllembxssdm  6335  tfrcllemaccex  6340  domen  6729  mapsnen  6789  xpsnen  6799  xpcomco  6804  xpassen  6808  fimax2gtri  6879  supelti  6979  cc1  7227  subhalfnqq  7376  ltbtwnnq  7378  prnmaxl  7450  prnminu  7451  prarloc  7465  genpdflem  7469  genpassl  7486  genpassu  7487  ltexprlemm  7562  2rexuz  9541  seq3f1olemp  10458  cbvsum  11323  cbvprod  11521  nnwosdc  11994  inffinp1  12384  ctiunctal  12396  unct  12397  isbasis2g  12837  tgval2  12845  ntreq0  12926  lmff  13043  metrest  13300  bj-axempty  13928  bj-axempty2  13929  bj-vprc  13931  bdinex1  13934  bj-zfpair2  13945  bj-uniex2  13951  bj-d0clsepcl  13960