Theorem exbii 1854

Description: Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)

Hypothesis

Ref	Expression
exbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
exbii	⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Proof of Theorem exbii

Step	Hyp	Ref	Expression
1		exbi 1853	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1804	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 205  ∃wex 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1787

This theorem is referenced by:  2exbii  1855  3exbii  1856  exanali  1866  exancom  1868  19.43  1889  19.41vv  1958  19.41vvv  1959  19.41vvvv  1960  exdistr  1962  exdistr2  1966  3exdistr  1968  19.12vvv  1996  excom13  2168  exrot4  2170  2sb5  2276  dfsb7  2280  eeor  2334  eeorOLD  2335  19.12vv  2349  eean  2350  eeeanv  2352  ee4anv  2353  2sb8ev  2356  equsexALT  2421  2sb5rf  2474  2sb8e  2537  mo4  2568  eu6lem  2575  eubii  2587  sb8eulem  2600  cbvmovw  2604  cbvmow  2605  eu1  2614  sbmo  2618  2moswapv  2633  2moswap  2648  euae  2663  elisset  2822  clabel  2887  sbabel  2943  sbabelOLD  2944  nabbi  3049  rexbii2  3178  rexcom4  3182  2ex2rexrot  3183  r2exlem  3233  r19.41v  3276  r19.41  3277  rexcom  3284  isset  3444  rexv  3456  cgsex4g  3475  cgsex4gOLD  3476  ceqsex2  3481  ceqsex2v  3482  ceqsex3v  3483  gencbvex  3487  spc3egv  3541  spc3gv  3542  ceqsrexv  3587  rexabOLD  3634  rexrab2  3641  euxfrw  3660  euxfr  3662  euind  3663  reu6  3665  reu3  3666  2reuswap  3685  2reuswap2  3686  reuind  3692  2reu5lem3  3696  2reu5  3697  2rmoswap  3700  sbcimdv  3795  sbcg  3800  sbccomlem  3808  rmo2  3825  rmoanim  3832  rmoanimALT  3833  rexun  4129  reupick3  4259  euelss  4261  ndisj  4307  abn0OLD  4321  pssnel  4410  rexsns  4611  exsnrex  4622  snprc  4659  euabsn2  4667  reusn  4669  eusn  4672  elpreqpr  4803  elunirab  4861  uniprg  4862  uniprOLD  4864  uniun  4870  uniin  4871  uni0b  4873  uniintsn  4924  iuncom4  4938  dfiun2g  4966  iunn0  5001  iunxiun  5031  disjor  5059  cbvopab2  5156  cbvopab2v  5160  unopab  5161  axrep1  5215  axrep4  5219  axrep5  5220  axrep6  5221  zfrep4  5224  axsepgfromrep  5225  axnulALT  5232  0ex  5235  vnex  5242  inex1  5245  inuni  5271  axpweq  5291  zfpow  5293  axpow2  5294  axpow3  5295  vpwex  5304  zfpair  5348  zfpair2  5357  eqvinop  5404  copsexgw  5407  copsexg  5408  opabn0  5468  iunopab  5474  dfid2  5491  dfid3  5492  opeliunxp  5654  xpiundi  5657  xpiundir  5658  elvvv  5662  csbxp  5685  eliunxp  5744  exopxfr  5750  relop  5757  opelco2g  5774  cnvco  5792  cnvuni  5793  dfdm3  5794  dfrn2  5795  dfrn3  5796  elrng  5798  dfdm4  5802  csbdm  5804  eldm2g  5806  dmun  5817  dmin  5818  dmiun  5820  dmuni  5821  dmopab  5822  dmi  5828  dmep  5830  domepOLD  5831  rnep  5834  rnopab  5861  dmcosseq  5880  dmres  5911  elsnres  5929  dfima2  5969  elima3  5974  imadmrn  5977  imai  5980  args  5998  rniun  6049  xpdifid  6069  ssrnres  6079  dmsnn0  6108  dmsnopg  6114  cnvresima  6131  mptpreima  6139  dfco2  6147  coundi  6149  coundir  6150  resco  6152  imaco  6153  rnco  6154  coiun  6158  coi1  6164  coass  6167  xpco  6190  elsnxp  6192  dfpo2  6197  dffun2  6441  dffun5  6444  imadif  6515  funimaexg  6517  brprcneu  6760  fvprc  6761  dffv2  6858  fndmin  6917  fvn0ssdmfun  6947  abrexco  7112  imaiun  7113  isomin  7202  dfoprab2  7325  cbvoprab2  7355  zfun  7581  uniex2  7583  uniuni  7604  elxp4  7757  elxp5  7758  fiun  7773  f1iun  7774  f11o  7777  fvresex  7790  opabex3d  7795  opabex3rd  7796  opabex3  7797  abexssex  7800  abexex  7801  oprabrexex2  7808  releldm2  7871  dfopab2  7879  dfoprab3s  7880  fsplit  7942  fsplitOLD  7943  frxp  7952  suppvalbr  7966  cnvimadfsn  7973  brtpos2  8033  dfwrecsOLD  8114  wfrfunOLD  8135  dfrecs3  8188  dfrecs3OLD  8189  oarec  8370  oeeu  8411  domen  8726  xpsnen  8817  xpcomco  8823  xpassen  8827  dif1en  8919  inf2  9351  zfinf  9367  axinf2  9368  zfinf2  9370  brttrcl2  9442  ttrcltr  9444  ttrclresv  9445  ttrclselem2  9454  rankuni  9614  scott0  9637  cp  9642  ween  9784  aceq1  9866  aceq0  9867  aceq2  9868  dfac5lem1  9872  dfac5lem2  9873  dfac5lem3  9874  kmlem3  9901  kmlem14  9912  kmlem15  9913  kmlem16  9914  cflem  9995  cf0  10000  cfval2  10009  cfss  10014  cfslb  10015  fin23lem32  10093  axdc2lem  10197  zfac  10209  ac9  10232  ac9s  10242  axpowndlem3  10348  zfcndrep  10363  zfcndun  10364  zfcndpow  10365  zfcndinf  10367  zfcndac  10368  axgroth5  10573  axgroth2  10574  axgroth6  10577  axgroth3  10580  axgroth4  10581  grothprim  10583  grothtsk  10584  genpass  10758  ltexprlem1  10785  ltexprlem4  10788  supaddc  11934  supadd  11935  supmul1  11936  supmullem2  11938  2rexuz  12631  nnwos  12646  hashgt23el  14129  hashfun  14142  wwlktovfo  14663  xpcogend  14675  cbvsum  15397  cbvprod  15615  iprodmul  15703  maxprmfct  16404  4sqlem12  16647  vdwmc  16669  cshwrepswhash1  16794  imasleval  17242  isacs2  17352  cicsym  17506  gsumval3eu  19495  lidlnz  20489  isbasis2g  22088  tgval2  22096  ntreq0  22218  lmff  22442  cmpfi  22549  is1stc2  22583  1stcelcls  22602  unisngl  22668  isfbas2  22976  elfg  23012  alexsubALTlem3  23190  ustfilxp  23354  metrest  23670  metuel2  23711  restmetu  23716  dchrvmasumlema  26638  istrkg2ld  26811  istrkg3ld  26812  1loopgrvd2  27860  wwlksnextsurj  28253  isgrpo  28847  nmo  30826  reuxfrdf  30827  rexunirn  30828  dmrab  30832  disjorf  30906  fcoinvbr  30935  mpomptxf  31004  cnvoprabOLD  31043  fpwrelmapffslem  31055  ordtconnlem1  31862  ddemeas  32192  omssubaddlem  32254  omssubadd  32255  eulerpartlemgvv  32331  bnj89  32688  bnj133  32694  bnj1019  32747  bnj1101  32752  bnj1109  32754  bnj1143  32758  bnj1198  32763  bnj1304  32787  bnj605  32875  bnj607  32884  bnj600  32887  bnj865  32891  bnj916  32901  bnj983  32919  bnj985v  32921  bnj985  32922  bnj996  32924  bnj1033  32937  bnj1083  32946  bnj1090  32947  bnj1093  32948  bnj1110  32950  bnj1128  32958  bnj1145  32961  bnj1171  32968  bnj1172  32969  bnj1174  32971  bnj1176  32973  bnj1186  32975  bnj1189  32977  bnj1253  32985  bnj1279  32986  bnj1371  32997  bnj1374  32999  bnj1312  33026  exdifsn  33041  fineqvrep  33052  fineqvpow  33053  lfuhgr3  33069  loop1cycl  33087  satfvsucsuc  33315  satf0op  33327  axextprim  33630  axrepprim  33631  axunprim  33632  axpowprim  33633  axregprim  33634  axinfprim  33635  axacprim  33636  imaeqsexv  33678  dftr6  33706  coep  33707  coepr  33708  dffr5  33709  cnvco1  33714  cnvco2  33715  eldm3  33716  fundmpss  33728  dfdm5  33735  dfrn5  33736  elima4  33738  axextdfeq  33761  19.12b  33765  axextndbi  33768  elold  34041  lrrecfr  34088  brtxp  34170  brpprod  34175  brsset  34179  dfon3  34182  brtxpsd  34184  elfix  34193  dffix2  34195  sscoid  34203  dffun10  34204  elfuns  34205  elsingles  34208  snelsingles  34212  dfiota3  34213  brimg  34227  brapply  34228  brcup  34229  brcap  34230  brsuccf  34231  funpartlem  34232  brrestrict  34239  dfrecs2  34240  dfrdg4  34241  neifg  34548  bj-equsexval  34829  bj-eeanvw  34883  bj-substw  34892  eliminable-abelv  35041  eliminable-abelab  35042  bj-denoteslem  35043  bj-rexvw  35053  bj-csbsnlem  35076  bj-gabima  35116  bj-snsetex  35141  bj-elsngl  35146  bj-snglc  35147  bj-clel3gALT  35209  bj-nul  35215  bj-dfid2ALT  35224  bj-restpw  35251  bj-restuni  35256  bj-dfmpoa  35277  bj-opabco  35347  bj-xpcossxp  35348  bj-imdirco  35349  mptsnunlem  35497  topdifinffinlem  35506  difunieq  35533  wl-dfclab  35735  poimirlem26  35791  ismblfin  35806  itg2addnclem3  35818  itg2addnc  35819  ismgmOLD  35996  sbcexfi  36263  sbccom2lem  36270  eldmres  36396  ecinn0  36473  ineleq  36474  moantr  36482  rnxrn  36512  rnxrnres  36513  dfcoss2  36527  dfcoss3  36528  1cossres  36540  cocossss  36547  rncossdmcoss  36561  eldmcoss2  36565  coss0  36585  cossid  36586  dfssr2  36605  eldmqs1cossres  36759  prtlem16  36871  prter2  36883  islshpat  37019  islpln5  37537  islvol5  37581  pmapglb  37772  polval2N  37908  cdlemftr3  38567  dibelval3  39149  dicelval3  39182  dihglb2  39344  sn-axrep5v  40174  prjspeclsp  40440  diophrex  40586  rp-isfinite6  41096  snen1g  41102  relintab  41153  imaiun1  41221  coiun1  41222  clsk3nimkb  41612  expandexn  41869  ismnuprim  41874  rr-groth  41879  ismnushort  41881  rr-grothshortbi  41883  19.36vv  41963  19.37vv  41965  pm11.58  41970  pm11.6  41972  pm13.192  41990  2sbc5g  41996  iotasbc2  42000  onfrALTlem5  42124  onfrALTlem1  42130  ax6e2nd  42140  2sb5nd  42142  en3lplem2VD  42426  onfrALTlem5VD  42467  relopabVD  42483  ax6e2ndVD  42490  2sb5ndVD  42492  ax6e2ndALT  42512  2sb5ndALT  42514  rfcnnnub  42541  inn0f  42583  stoweidlem34  43538  stoweidlem35  43539  stoweidlem60  43564  smfpimcc  44301  ichexmpl1  44882  sprid  44887  opeliun2xp  45629  eliunxp2  45630  rextru  46110  mosssn2  46123  setrec1lem3  46356  elpglem3  46379  eximp-surprise  46449