Theorem exbii 1651

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2exbii  1652  3exbii  1653  exancom  1654  excom13  1735  exrot4  1737  eeor  1741  sbcof2  1856  sbequ8  1893  sbidm  1897  sborv  1937  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1956  19.42vvv  1959  exdistr2  1961  3exdistr  1962  4exdistr  1963  eean  1982  eeeanv  1984  ee4anv  1985  2sb5  2034  2sb5rf  2040  sbel2x  2049  sbexyz  2054  sbex  2055  exsb  2059  2exsb  2060  sb8eu  2090  sb8euh  2100  eu1  2102  eu2  2122  2moswapdc  2168  2exeu  2170  exists1  2174  clelab  2355  clabel  2356  sbabel  2399  rexbii2  2541  r2exf  2548  nfrexdya  2566  r19.41  2686  r19.43  2689  cbvreuvw  2771  isset  2806  rexv  2818  ceqsex2  2841  ceqsex3v  2843  gencbvex  2847  ceqsrexv  2933  rexab  2965  rexrab2  2970  euxfrdc  2989  euind  2990  reu6  2992  reu3  2993  2reuswapdc  3007  reuind  3008  sbccomlem  3103  rmo2ilem  3119  rexun  3384  reupick3  3489  abn0r  3516  abn0m  3517  rabn0m  3519  rexsns  3705  exsnrex  3708  snprc  3731  euabsn2  3735  reusn  3737  eusn  3740  snmb  3788  elunirab  3901  unipr  3902  uniun  3907  uniin  3908  iuncom4  3972  dfiun2g  3997  iunn0m  4026  iunxiun  4047  disjnim  4073  cbvopab2  4158  cbvopab2v  4161  unopab  4163  zfnuleu  4208  0ex  4211  vnex  4215  inex1  4218  intexabim  4236  iinexgm  4238  inuni  4239  unidif0  4251  axpweq  4255  zfpow  4259  axpow2  4260  axpow3  4261  vpwex  4263  zfpair2  4294  mss  4312  exss  4313  opm  4320  eqvinop  4329  copsexg  4330  opabm  4369  iunopab  4370  zfun  4525  uniex2  4527  uniuni  4542  rexxfrd  4554  dtruex  4651  zfinf2  4681  elxp2  4737  opeliunxp  4774  xpiundi  4777  xpiundir  4778  elvvv  4782  eliunxp  4861  rexiunxp  4864  relop  4872  elco  4888  opelco2g  4890  cnvco  4907  cnvuni  4908  dfdm3  4909  dfrn2  4910  dfrn3  4911  elrng  4913  dfdm4  4915  eldm2g  4919  dmun  4930  dmin  4931  dmiun  4932  dmuni  4933  dmopab  4934  dmi  4938  reldmm  4942  dmmrnm  4943  elrn  4967  rnopab  4971  dmcosseq  4996  dmres  5026  elres  5041  elsnres  5042  dfima2  5070  elima3  5075  imadmrn  5078  imai  5084  args  5097  rniun  5139  ssrnres  5171  dmsnm  5194  dmsnopg  5200  elxp4  5216  elxp5  5217  cnvresima  5218  mptpreima  5222  dfco2  5228  coundi  5230  coundir  5231  resco  5233  imaco  5234  rnco  5235  coiun  5238  coi1  5244  coass  5247  xpcom  5275  dffun2  5328  imadif  5401  imainlem  5402  funimaexglem  5404  fun11iun  5593  f11o  5605  brprcneu  5620  nfvres  5663  fndmin  5742  abrexco  5883  imaiun  5884  dfoprab2  6051  cbvoprab2  6077  rexrnmpo  6120  opabex3d  6266  opabex3  6267  abexssex  6270  abexex  6271  oprabrexex2  6275  uchoice  6283  releldm2  6331  dfopab2  6335  dfoprab3s  6336  cnvoprab  6380  brtpos2  6397  tfr1onlemaccex  6494  tfrcllembxssdm  6502  tfrcllemaccex  6507  domen  6900  mapsnen  6964  xpsnen  6980  xpcomco  6985  xpassen  6989  fimax2gtri  7063  supelti  7169  cc1  7451  subhalfnqq  7601  ltbtwnnq  7603  prnmaxl  7675  prnminu  7676  prarloc  7690  genpdflem  7694  genpassl  7711  genpassu  7712  ltexprlemm  7787  2rexuz  9777  seq3f1olemp  10737  cbvsum  11871  cbvprod  12069  nnwosdc  12560  4sqlem12  12925  inffinp1  13000  ctiunctal  13012  unct  13013  isbasis2g  14719  tgval2  14725  ntreq0  14806  lmff  14923  metrest  15180  upgrex  15903  bj-axempty  16256  bj-axempty2  16257  bj-vprc  16259  bdinex1  16262  bj-zfpair2  16273  bj-uniex2  16279  bj-d0clsepcl  16288