Theorem exbii 1774

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

Syntax hints:   <-> wb 196   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  2exbii  1775  3exbii  1776  exanali  1786  exancom  1787  19.43  1810  sbequ8  1885  19.12vvv  1907  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistr  1919  19.42vvv  1921  exdistr2  1922  3exdistr  1923  equsexvw  1932  excom13  2044  exrot4  2046  equsexv  2109  eeor  2171  19.12vv  2180  eean  2181  eeeanv  2183  ee4anv  2184  equsexALT  2293  2sb5  2443  2sb5rf  2451  2sb8e  2467  sb8eu  2503  eu1  2510  sbmo  2515  2moswap  2547  exists1  2561  clabel  2749  sbabel  2793  nabbi  2896  rexbii2  3039  r2exlem  3059  r19.41v  3089  r19.41  3090  isset  3207  rexv  3220  ceqsex2  3244  ceqsex3v  3246  gencbvex  3250  vtocl2  3261  vtocl3  3262  spc3gv  3298  ceqsrexv  3336  rexab  3369  rexrab2  3374  euxfr  3392  euind  3393  reu6  3395  reu3  3396  2reuswap  3410  reuind  3411  2reu5lem3  3415  2reu5  3416  sbccomlem  3508  rmo2  3526  rexun  3793  reupick3  3912  euelss  3914  abn0  3954  pssnel  4039  rexsns  4217  exsnrex  4221  snprc  4253  euabsn2  4260  reusn  4262  eusn  4265  elpreqpr  4396  elunirab  4448  unipr  4449  uniun  4456  uniin  4457  uni0b  4463  uniintsn  4514  iuncom4  4528  dfiun2g  4552  iunn0  4580  iunxiun  4608  disjor  4634  cbvopab2  4724  cbvopab2v  4727  unopab  4728  axrep1  4772  axrep4  4775  axrep5  4776  zfrep4  4779  axsep  4780  zfnuleu  4786  axnulALT  4787  0ex  4790  vprc  4796  inex1  4799  inuni  4826  axpweq  4842  zfpow  4844  axpow2  4845  axpow3  4846  pwex  4848  zfpair  4904  zfpair2  4907  eqvinop  4955  copsexg  4956  opabn0  5006  iunopab  5012  dfid3  5025  elxp2OLD  5133  opeliunxp  5170  xpiundi  5173  xpiundir  5174  elvvv  5178  csbxp  5200  eliunxp  5259  exopxfr  5265  relop  5272  opelco2g  5289  cnvco  5308  cnvuni  5309  dfdm3  5310  dfrn2  5311  dfrn3  5312  elrng  5314  dfdm4  5316  csbdm  5318  eldm2g  5320  dmun  5331  dmin  5332  dmiun  5333  dmuni  5334  dmopab  5335  dmi  5340  elrn  5366  rnopab  5370  dmcosseq  5387  dmres  5419  elres  5435  elsnres  5436  dfima2  5468  elima3  5473  imadmrn  5476  imai  5478  args  5493  rniun  5543  xpdifid  5562  ssrnres  5572  dmsnn0  5600  dmsnopg  5606  cnvresima  5623  mptpreima  5628  dfco2  5634  coundi  5636  coundir  5637  resco  5639  imaco  5640  rnco  5641  coiun  5645  coi1  5651  coass  5654  xpco  5675  elsnxp  5677  elsnxpOLD  5678  dffun2  5898  dffun5  5901  imadif  5973  funimaexg  5975  brprcneu  6184  dffv2  6271  fndmin  6324  fvn0ssdmfun  6350  abrexco  6502  imaiun  6503  isomin  6587  dfoprab2  6701  cbvoprab2  6728  zfun  6950  uniex2  6952  uniuni  6971  elxp4  7110  elxp5  7111  fun11iun  7126  f11o  7128  fvresex  7139  opabex3d  7145  opabex3  7146  abexssex  7149  abexex  7151  oprabrexex2  7158  releldm2  7218  dfopab2  7222  dfoprab3s  7223  fsplit  7282  frxp  7287  suppvalbr  7299  cnvimadfsn  7304  brtpos2  7358  wfrfun  7425  dfrecs3  7469  oarec  7642  oeeu  7683  domen  7968  mapsnen  8035  xpsnen  8044  xpcomco  8050  xpassen  8054  inf2  8520  zfinf  8536  axinf2  8537  zfinf2  8539  rankuni  8726  scott0  8749  cp  8754  ween  8858  aceq1  8940  aceq0  8941  aceq2  8942  dfac5lem1  8946  dfac5lem2  8947  dfac5lem3  8948  kmlem3  8974  kmlem14  8985  kmlem15  8986  kmlem16  8987  cflem  9068  cf0  9073  cfval2  9082  cfss  9087  cfslb  9088  fin23lem32  9166  axdc2lem  9270  zfac  9282  ac9  9305  ac9s  9315  axpowndlem3  9421  zfcndrep  9436  zfcndun  9437  zfcndpow  9438  zfcndinf  9440  zfcndac  9441  axgroth5  9646  axgroth2  9647  grothpw  9648  axgroth6  9650  axgroth3  9653  axgroth4  9654  grothprim  9656  grothtsk  9657  genpass  9831  ltexprlem1  9858  ltexprlem4  9861  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  2rexuz  11740  nnwos  11755  hashfun  13224  wwlktovfo  13701  xpcogend  13713  cbvsum  14425  cbvprod  14645  iprodmul  14734  maxprmfct  15421  4sqlem12  15660  vdwmc  15682  cshwrepswhash1  15809  imasleval  16201  isacs2  16314  cicsym  16464  gsumval3eu  18305  lidlnz  19228  isbasis2g  20752  tgval2  20760  ntreq0  20881  lmff  21105  cmpfi  21211  is1stc2  21245  1stcelcls  21264  unisngl  21330  isfbas2  21639  elfg  21675  alexsubALTlem3  21853  ustfilxp  22016  metrest  22329  metuel2  22370  restmetu  22375  cmetss  23113  dchrvmasumlema  25189  istrkg2ld  25359  istrkg3ld  25360  1loopgrvd2  26399  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnextsur  26795  isgrpo  27351  nmo  29325  2reuswap2  29328  rexunirn  29331  disjorf  29392  fcoinvbr  29419  mpt2mptxf  29477  cnvoprab  29498  fpwrelmapffslem  29507  ordtconnlem1  29970  ddemeas  30299  omssubaddlem  30361  omssubadd  30362  eulerpartlemgvv  30438  bnj89  30787  bnj133  30793  bnj1019  30850  bnj1101  30855  bnj1109  30857  bnj1143  30861  bnj1198  30866  bnj1304  30890  bnj605  30977  bnj607  30986  bnj600  30989  bnj865  30993  bnj916  31003  bnj983  31021  bnj985  31023  bnj996  31025  bnj1033  31037  bnj1083  31046  bnj1090  31047  bnj1093  31048  bnj1110  31050  bnj1128  31058  bnj1145  31061  bnj1171  31068  bnj1172  31069  bnj1174  31071  bnj1176  31073  bnj1186  31075  bnj1189  31077  bnj1253  31085  bnj1279  31086  bnj1371  31097  bnj1374  31099  bnj1312  31126  axextprim  31578  axrepprim  31579  axunprim  31580  axpowprim  31581  axregprim  31582  axinfprim  31583  axacprim  31584  dftr6  31640  coep  31641  coepr  31642  dffr5  31643  dfpo2  31645  cnvco1  31649  cnvco2  31650  eldm3  31651  fundmpss  31664  dfdm5  31676  dfrn5  31677  elima4  31679  domep  31698  axextdfeq  31703  19.12b  31707  axextndbi  31710  frrlem5c  31786  brtxp  31987  brpprod  31992  brsset  31996  dfon3  31999  brtxpsd  32001  elfix  32010  dffix2  32012  sscoid  32020  dffun10  32021  elfuns  32022  elsingles  32025  snelsingles  32029  dfiota3  32030  brimg  32044  brapply  32045  brcup  32046  brcap  32047  brsuccf  32048  funpartlem  32049  brrestrict  32056  dfrecs2  32057  dfrdg4  32058  neifg  32366  bj-equsexval  32638  bj-dfssb2  32640  bj-eeanvw  32704  bj-clabel  32783  bj-axrep1  32788  bj-axrep4  32791  bj-axrep5  32792  bj-axsep  32793  bj-zfpow  32795  bj-cleljustab  32847  bj-denotes  32858  bj-rexvwv  32866  bj-rexcom4  32869  bj-csbsnlem  32898  bj-snsetex  32951  bj-elsngl  32956  bj-snglc  32957  bj-nul  33018  bj-restpw  33045  bj-restuni  33050  bj-dfmpt2a  33071  mptsnunlem  33185  topdifinffinlem  33195  poimirlem26  33435  ismblfin  33450  itg2addnclem3  33463  itg2addnc  33464  ismgmOLD  33649  sbcexfi  33920  sbccom2lem  33929  eldmres  34036  ecinn0  34118  ineleq  34119  motr  34127  prtlem16  34154  prter2  34166  islshpat  34304  islpln5  34821  islvol5  34865  pmapglb  35056  polval2N  35192  cdlemftr3  35853  dibelval3  36436  dicelval3  36469  dihglb2  36631  diophrex  37339  rp-isfinite6  37864  relintab  37889  imaiun1  37943  coiun1  37944  ndisj  38063  clsk3nimkb  38338  19.36vv  38582  19.37vv  38584  pm11.58  38590  pm11.6  38592  pm13.192  38611  2sbc5g  38617  iotasbc2  38621  onfrALTlem5  38757  onfrALTlem1  38763  ax6e2nd  38774  2sb5nd  38776  en3lplem2VD  39079  relopabVD  39137  ax6e2ndVD  39144  2sb5ndVD  39146  ax6e2ndALT  39166  2sb5ndALT  39168  rfcnnnub  39195  inn0f  39242  stoweidlem34  40251  stoweidlem35  40252  stoweidlem60  40277  smfpimcc  41014  rmoanim  41179  2rmoswap  41184  sprid  41724  opeliun2xp  42111  eliunxp2  42112  setrec1lem3  42436  elpglem3  42456  eximp-surprise  42530