Theorem exbii 1658

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1659  3exbii  1660  exancom  1661  excom13  1741  exrot4  1743  eeor  1747  sbcof2  1863  sbequ8  1900  sbidm  1904  sborv  1945  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistr  1965  19.42vvv  1968  exdistr2  1970  3exdistr  1971  4exdistr  1972  eean  1991  eeeanv  1993  ee4anv  1994  2sb5  2043  2sb5rf  2049  sbel2x  2058  sbexyz  2063  sbex  2064  exsb  2068  2exsb  2069  sb8eu  2099  sb8euh  2109  eu1  2111  eu2  2131  2moswapdc  2177  2exeu  2179  exists1  2183  clelab  2366  clabel  2367  sbabel  2419  rexbii2  2561  r2exf  2568  nfrexdya  2586  r19.41  2706  r19.43  2709  cbvreuvw  2792  isset  2828  rexv  2840  ceqsex2  2863  ceqsex3v  2865  gencbvex  2869  ceqsrexv  2956  rexab  2988  rexrab2  2993  euxfrdc  3012  euind  3013  reu6  3015  reu3  3016  2reuswapdc  3030  reuind  3031  sbccomlem  3126  rmo2ilem  3142  rexun  3409  reupick3  3518  abn0r  3546  abn0m  3547  rabn0m  3549  rexsns  3747  exsnrex  3750  snprc  3773  euabsn2  3779  reusn  3781  eusn  3784  snmb  3832  elunirab  3946  unipr  3947  uniun  3952  uniin  3953  iuncom4  4017  dfiun2g  4042  iunn0m  4071  iunxiun  4092  disjnim  4118  cbvopab2  4203  cbvopab2v  4206  unopab  4208  zfnuleu  4255  0ex  4258  vnex  4262  inex1  4265  intexabim  4286  iinexgm  4288  inuni  4289  unidif0  4302  axpweq  4306  zfpow  4310  axpow2  4311  axpow3  4312  vpwex  4314  zfpair2  4345  mss  4364  exss  4365  opm  4372  eqvinop  4381  copsexg  4382  opabm  4421  iunopab  4422  zfun  4577  uniex2  4579  uniex2OLD  4580  uniuni  4595  rexxfrd  4607  dtruex  4704  zfinf2  4734  elxp2  4790  opeliunxp  4828  xpiundi  4831  xpiundir  4832  elvvv  4836  eliunxp  4917  rexiunxp  4920  relop  4928  elco  4944  opelco2g  4946  cnvco  4963  cnvuni  4964  dfdm3  4965  dfrn2  4966  dfrn3  4967  elrng  4969  dfdm4  4971  eldm2g  4975  dmun  4986  dmin  4987  dmiun  4988  dmuni  4989  dmopab  4990  dmi  4994  reldmm  4998  dmmrnm  4999  elrn  5023  rnopab  5027  dmcosseq  5052  dmres  5082  elres  5097  elsnres  5098  dfima2  5126  elima3  5131  imadmrn  5134  imai  5141  args  5154  rniun  5196  ssrnres  5228  dmsnm  5251  dmsnopg  5257  elxp4  5273  elxp5  5274  cnvresima  5275  mptpreima  5279  dfco2  5285  coundi  5287  coundir  5288  resco  5290  imaco  5291  rnco  5292  coiun  5295  coi1  5301  coass  5304  xpcom  5332  dffun2  5385  imadif  5459  imainlem  5460  funimaexglem  5462  fun11iun  5658  f11o  5671  brprcneu  5686  nfvres  5729  fndmin  5810  abrexco  5958  imaiun  5959  dfoprab2  6128  cbvoprab2  6154  rexrnmpo  6197  opabex3d  6343  opabex3  6344  abexssex  6347  abexex  6348  oprabrexex2  6356  uchoice  6364  releldm2  6412  dfopab2  6416  dfoprab3s  6417  cnvoprab  6463  cnvimadfsn  6478  brtpos2  6515  tfr1onlemaccex  6612  tfrcllembxssdm  6620  tfrcllemaccex  6625  domen  7028  mapsnen  7093  xpsnen  7112  xpcomco  7117  xpassen  7121  fimax2gtri  7199  supelti  7335  cc1  7624  subhalfnqq  7774  ltbtwnnq  7776  prnmaxl  7848  prnminu  7849  prarloc  7863  genpdflem  7867  genpassl  7884  genpassu  7885  ltexprlemm  7960  2rexuz  9964  seq3f1olemp  10933  cbvsum  12107  cbvprod  12306  nnwosdc  12797  4sqlem12  13162  inffinp1  13301  ctiunctal  13313  unct  13314  isbasis2g  15072  tgval2  15078  ntreq0  15159  lmff  15276  metrest  15533  upgrex  16261  1loopgrvd2fi  16463  bj-axempty  16836  bj-axempty2  16837  bj-vprc  16839  bdinex1  16842  bj-zfpair2  16853  bj-uniex2  16859  bj-d0clsepcl  16868  alsbii  17049