Theorem exbii 1629

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

Syntax hints:   <-> wb 105   E.wex 1516

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1630  3exbii  1631  exancom  1632  excom13  1713  exrot4  1715  eeor  1719  sbcof2  1834  sbequ8  1871  sbidm  1875  sborv  1915  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistr  1934  19.42vvv  1937  exdistr2  1939  3exdistr  1940  4exdistr  1941  eean  1960  eeeanv  1962  ee4anv  1963  2sb5  2012  2sb5rf  2018  sbel2x  2027  sbexyz  2032  sbex  2033  exsb  2037  2exsb  2038  sb8eu  2068  sb8euh  2078  eu1  2080  eu2  2100  2moswapdc  2146  2exeu  2148  exists1  2152  clelab  2333  clabel  2334  sbabel  2377  rexbii2  2519  r2exf  2526  nfrexdya  2544  r19.41  2663  r19.43  2666  cbvreuvw  2748  isset  2783  rexv  2795  ceqsex2  2818  ceqsex3v  2820  gencbvex  2824  ceqsrexv  2910  rexab  2942  rexrab2  2947  euxfrdc  2966  euind  2967  reu6  2969  reu3  2970  2reuswapdc  2984  reuind  2985  sbccomlem  3080  rmo2ilem  3096  rexun  3361  reupick3  3466  abn0r  3493  abn0m  3494  rabn0m  3496  rexsns  3682  exsnrex  3685  snprc  3708  euabsn2  3712  reusn  3714  eusn  3717  snmb  3764  elunirab  3877  unipr  3878  uniun  3883  uniin  3884  iuncom4  3948  dfiun2g  3973  iunn0m  4002  iunxiun  4023  disjnim  4049  cbvopab2  4134  cbvopab2v  4137  unopab  4139  zfnuleu  4184  0ex  4187  vnex  4191  inex1  4194  intexabim  4212  iinexgm  4214  inuni  4215  unidif0  4227  axpweq  4231  zfpow  4235  axpow2  4236  axpow3  4237  vpwex  4239  zfpair2  4270  mss  4288  exss  4289  opm  4296  eqvinop  4305  copsexg  4306  opabm  4345  iunopab  4346  zfun  4499  uniex2  4501  uniuni  4516  rexxfrd  4528  dtruex  4625  zfinf2  4655  elxp2  4711  opeliunxp  4748  xpiundi  4751  xpiundir  4752  elvvv  4756  eliunxp  4835  rexiunxp  4838  relop  4846  elco  4862  opelco2g  4864  cnvco  4881  cnvuni  4882  dfdm3  4883  dfrn2  4884  dfrn3  4885  elrng  4887  dfdm4  4889  eldm2g  4893  dmun  4904  dmin  4905  dmiun  4906  dmuni  4907  dmopab  4908  dmi  4912  dmmrnm  4916  elrn  4940  rnopab  4944  dmcosseq  4969  dmres  4999  elres  5014  elsnres  5015  dfima2  5043  elima3  5048  imadmrn  5051  imai  5057  args  5070  rniun  5112  ssrnres  5144  dmsnm  5167  dmsnopg  5173  elxp4  5189  elxp5  5190  cnvresima  5191  mptpreima  5195  dfco2  5201  coundi  5203  coundir  5204  resco  5206  imaco  5207  rnco  5208  coiun  5211  coi1  5217  coass  5220  xpcom  5248  dffun2  5300  imadif  5373  imainlem  5374  funimaexglem  5376  fun11iun  5565  f11o  5577  brprcneu  5592  nfvres  5633  fndmin  5710  abrexco  5851  imaiun  5852  dfoprab2  6015  cbvoprab2  6041  rexrnmpo  6084  opabex3d  6229  opabex3  6230  abexssex  6233  abexex  6234  oprabrexex2  6238  uchoice  6246  releldm2  6294  dfopab2  6298  dfoprab3s  6299  cnvoprab  6343  brtpos2  6360  tfr1onlemaccex  6457  tfrcllembxssdm  6465  tfrcllemaccex  6470  domen  6863  mapsnen  6927  xpsnen  6941  xpcomco  6946  xpassen  6950  fimax2gtri  7024  supelti  7130  cc1  7412  subhalfnqq  7562  ltbtwnnq  7564  prnmaxl  7636  prnminu  7637  prarloc  7651  genpdflem  7655  genpassl  7672  genpassu  7673  ltexprlemm  7748  2rexuz  9738  seq3f1olemp  10697  cbvsum  11786  cbvprod  11984  nnwosdc  12475  4sqlem12  12840  inffinp1  12915  ctiunctal  12927  unct  12928  isbasis2g  14632  tgval2  14638  ntreq0  14719  lmff  14836  metrest  15093  upgrex  15814  bj-axempty  16028  bj-axempty2  16029  bj-vprc  16031  bdinex1  16034  bj-zfpair2  16045  bj-uniex2  16051  bj-d0clsepcl  16060