Theorem exbii 1582

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

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

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1487  ax-ial 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2exbii  1583  3exbii  1584  exancom  1585  excom13  1666  exrot4  1668  eeor  1672  sbcof2  1787  sbequ8  1824  sbidm  1828  sborv  1867  19.41vv  1880  19.41vvv  1881  19.41vvvv  1882  exdistr  1886  19.42vvv  1889  exdistr2  1891  3exdistr  1892  4exdistr  1893  eean  1908  eeeanv  1910  ee4anv  1911  2sb5  1960  2sb5rf  1966  sbel2x  1975  sbexyz  1980  sbex  1981  exsb  1985  2exsb  1986  sb8eu  2016  sb8euh  2026  eu1  2028  eu2  2047  2moswapdc  2093  2exeu  2095  exists1  2099  clelab  2280  clabel  2281  sbabel  2323  rexbii2  2465  r2exf  2472  nfrexdya  2490  r19.41  2609  r19.43  2612  cbvreuvw  2683  isset  2715  rexv  2727  ceqsex2  2749  ceqsex3v  2751  gencbvex  2755  ceqsrexv  2839  rexab  2870  rexrab2  2875  euxfrdc  2894  euind  2895  reu6  2897  reu3  2898  2reuswapdc  2912  reuind  2913  sbccomlem  3007  rmo2ilem  3022  rexun  3283  reupick3  3388  abn0r  3414  abn0m  3415  rabn0m  3417  rexsns  3594  exsnrex  3597  snprc  3620  euabsn2  3624  reusn  3626  eusn  3629  elunirab  3781  unipr  3782  uniun  3787  uniin  3788  iuncom4  3852  dfiun2g  3877  iunn0m  3905  iunxiun  3926  disjnim  3952  cbvopab2  4034  cbvopab2v  4037  unopab  4039  zfnuleu  4084  0ex  4087  vnex  4091  inex1  4094  intexabim  4109  iinexgm  4111  inuni  4112  unidif0  4123  axpweq  4127  zfpow  4131  axpow2  4132  axpow3  4133  vpwex  4135  zfpair2  4165  mss  4181  exss  4182  opm  4189  eqvinop  4198  copsexg  4199  opabm  4235  iunopab  4236  zfun  4389  uniex2  4391  uniuni  4405  rexxfrd  4417  dtruex  4512  zfinf2  4542  elxp2  4597  opeliunxp  4634  xpiundi  4637  xpiundir  4638  elvvv  4642  eliunxp  4718  rexiunxp  4721  relop  4729  elco  4745  opelco2g  4747  cnvco  4764  cnvuni  4765  dfdm3  4766  dfrn2  4767  dfrn3  4768  elrng  4770  dfdm4  4771  eldm2g  4775  dmun  4786  dmin  4787  dmiun  4788  dmuni  4789  dmopab  4790  dmi  4794  dmmrnm  4798  elrn  4822  rnopab  4826  dmcosseq  4850  dmres  4880  elres  4895  elsnres  4896  dfima2  4923  elima3  4928  imadmrn  4931  imai  4935  args  4948  rniun  4989  ssrnres  5021  dmsnm  5044  dmsnopg  5050  elxp4  5066  elxp5  5067  cnvresima  5068  mptpreima  5072  dfco2  5078  coundi  5080  coundir  5081  resco  5083  imaco  5084  rnco  5085  coiun  5088  coi1  5094  coass  5097  xpcom  5125  dffun2  5173  imadif  5243  imainlem  5244  funimaexglem  5246  fun11iun  5428  f11o  5440  brprcneu  5454  nfvres  5494  fndmin  5567  abrexco  5700  imaiun  5701  dfoprab2  5858  cbvoprab2  5884  rexrnmpo  5926  opabex3d  6059  opabex3  6060  abexssex  6063  abexex  6064  oprabrexex2  6068  releldm2  6123  dfopab2  6127  dfoprab3s  6128  cnvoprab  6171  brtpos2  6188  tfr1onlemaccex  6285  tfrcllembxssdm  6293  tfrcllemaccex  6298  domen  6685  mapsnen  6745  xpsnen  6755  xpcomco  6760  xpassen  6764  fimax2gtri  6835  supelti  6934  cc1  7164  subhalfnqq  7313  ltbtwnnq  7315  prnmaxl  7387  prnminu  7388  prarloc  7402  genpdflem  7406  genpassl  7423  genpassu  7424  ltexprlemm  7499  2rexuz  9472  seq3f1olemp  10379  cbvsum  11234  cbvprod  11432  inffinp1  12109  ctiunctal  12121  unct  12122  isbasis2g  12382  tgval2  12390  ntreq0  12471  lmff  12588  metrest  12845  bj-axempty  13406  bj-axempty2  13407  bj-vprc  13409  bdinex1  13412  bj-zfpair2  13423  bj-uniex2  13429  bj-d0clsepcl  13438