Theorem exbii 1843

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 1842	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2		exbii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1792	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 205  ∃wex 1774

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

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

This theorem is referenced by:  2exbii  1844  3exbii  1845  exanali  1855  exancom  1857  19.43  1878  19.41vv  1947  19.41vvv  1948  19.41vvvv  1949  exdistr  1951  exdistr2  1955  3exdistr  1957  19.12vvv  1985  excom13  2154  exrot4  2156  2sb5  2267  dfsb7  2269  eeor  2325  eeorOLD  2326  19.12vv  2339  eean  2340  eeeanv  2342  ee4anv  2343  2sb8ef  2348  equsexALT  2414  2sb5rf  2467  2sb8e  2525  mo4  2556  eu6lem  2563  eubii  2575  sb8eulem  2588  cbvmovw  2592  cbvmow  2593  eu1  2602  sbmo  2606  2moswapv  2621  2moswap  2636  euae  2651  issetlem  2809  clabel  2877  sbabel  2934  sbabelOLD  2935  nabbib  3041  rextru  3073  rexbii2  3086  r2exlem  3139  r19.41v  3184  r19.41  3256  rexcom4  3281  rexcomOLD  3284  2ex2rexrot  3291  rexv  3496  cgsex4gOLD  3518  cgsex4gOLDOLD  3519  ceqsex2  3526  ceqsex2v  3527  ceqsex3v  3528  gencbvex  3532  spc3egv  3589  spc3gv  3590  ceqsrexv  3640  rexabOLD  3689  rexrab2  3694  euxfrw  3715  euxfr  3717  euind  3718  reu6  3720  reu3  3721  2reuswap  3740  2reuswap2  3741  reuind  3747  2reu5lem3  3751  2reu5  3752  2rmoswap  3755  sbcimdv  3848  sbcg  3853  sbccomlem  3861  rmo2  3878  rmoanim  3885  rmoanimALT  3886  rexun  4186  reupick3  4315  euelss  4317  ndisj  4363  abn0OLD  4377  pssnel  4466  rexsns  4669  exsnrex  4680  snprc  4717  euabsn2  4725  reusn  4727  eusn  4730  elpreqpr  4863  elunirab  4918  uniprg  4919  uniprOLD  4921  uniun  4928  uniin  4929  uni0b  4931  uniintsn  4985  iuncom4  4999  dfiun2g  5027  dfiun2gOLD  5028  iunn0  5064  iunxiun  5094  disjor  5122  cbvopab2  5219  cbvopab2v  5223  unopab  5224  axrep1  5280  axrep4  5284  axrep5  5285  axrep6  5286  zfrep4  5290  axsepgfromrep  5291  axnulALT  5298  0ex  5301  vnex  5308  inex1  5311  inuni  5339  axpweq  5344  zfpow  5360  axpow2  5361  axpow3  5362  vpwex  5371  zfpair  5415  zfpair2  5424  el  5433  eqvinop  5483  copsexgw  5486  copsexg  5487  opabn0  5549  iunopab  5555  iunopabOLD  5556  dfid2  5572  dfid3  5573  opeliunxp  5739  xpiundi  5742  xpiundir  5743  elvvv  5747  csbxp  5771  eliunxp  5834  exopxfr  5840  relop  5847  opelco2g  5864  cnvco  5882  cnvuni  5883  dfdm3  5884  dfrn2  5885  dfrn3  5886  elrng  5888  dfdm4  5892  csbdm  5894  eldm2g  5896  dmun  5907  dmin  5908  dmiun  5910  dmuni  5911  dmopab  5912  dmi  5918  dmep  5920  rnep  5923  rnopab  5950  dmcosseq  5970  dmres  6001  elsnres  6019  dfima2  6059  elima3  6064  imadmrn  6067  imai  6071  args  6090  rniun  6146  xpdifid  6166  ssrnres  6176  dmsnn0  6205  dmsnopg  6211  cnvresima  6228  mptpreima  6236  dfco2  6243  coundi  6245  coundir  6246  resco  6248  imaco  6249  rnco  6250  coiun  6254  coi1  6260  coass  6263  xpco  6287  elsnxp  6289  dfpo2  6294  dffun2OLDOLD  6554  dffun5  6559  imadif  6631  funimaexgOLD  6634  brprcneu  6881  brprcneuALT  6882  dffv2  6987  fndmin  7048  fvn0ssdmfun  7078  abrexco  7248  imaiun  7249  isomin  7339  imaeqsexv  7365  dfoprab2  7472  cbvoprab2  7502  zfun  7735  uniex2  7737  uniuni  7758  elxp4  7924  elxp5  7925  fiun  7940  f1iun  7941  f11o  7944  fvresex  7957  opabex3d  7963  opabex3rd  7964  opabex3  7965  abexssex  7968  abexex  7969  oprabrexex2  7976  releldm2  8041  dfopab2  8050  dfoprab3s  8051  fsplit  8116  frxp  8125  suppvalbr  8163  cnvimadfsn  8170  brtpos2  8231  dfwrecsOLD  8312  wfrfunOLD  8333  dfrecs3  8386  dfrecs3OLD  8387  oarec  8576  oeeu  8617  domen  8975  xpsnen  9073  xpcomco  9080  xpassen  9084  dif1enOLD  9180  inf2  9640  zfinf  9656  axinf2  9657  zfinf2  9659  brttrcl2  9731  ttrcltr  9733  ttrclresv  9734  ttrclselem2  9743  rankuni  9880  scott0  9903  cp  9908  ween  10052  aceq1  10134  aceq0  10135  aceq2  10136  dfac5lem1  10140  dfac5lem2  10141  dfac5lem3  10142  kmlem3  10169  kmlem14  10180  kmlem15  10181  kmlem16  10182  cflem  10263  cf0  10268  cfval2  10277  cfss  10282  cfslb  10283  fin23lem32  10361  axdc2lem  10465  zfac  10477  ac9  10500  ac9s  10510  axpowndlem3  10616  zfcndrep  10631  zfcndun  10632  zfcndpow  10633  zfcndinf  10635  zfcndac  10636  axgroth5  10841  axgroth2  10842  axgroth6  10845  axgroth3  10848  axgroth4  10849  grothprim  10851  grothtsk  10852  genpass  11026  ltexprlem1  11053  ltexprlem4  11056  supaddc  12205  supadd  12206  supmul1  12207  supmullem2  12209  2rexuz  12908  nnwos  12923  hashgt23el  14409  hashfun  14422  wwlktovfo  14935  xpcogend  14947  cbvsum  15667  cbvprod  15885  iprodmul  15973  maxprmfct  16673  4sqlem12  16918  vdwmc  16940  cshwrepswhash1  17065  imasleval  17516  isacs2  17626  cicsym  17780  gsumval3eu  19852  lidlnz  21130  isbasis2g  22844  tgval2  22852  ntreq0  22974  lmff  23198  cmpfi  23305  is1stc2  23339  1stcelcls  23358  unisngl  23424  isfbas2  23732  elfg  23768  alexsubALTlem3  23946  ustfilxp  24110  metrest  24426  metuel2  24467  restmetu  24472  dchrvmasumlema  27426  elold  27789  lrrecfr  27853  sleadd1  27899  addsuniflem  27911  addsasslem1  27913  addsasslem2  27914  mulsuniflem  28042  addsdilem1  28044  addsdilem2  28045  mulsasslem1  28056  mulsasslem2  28057  renegscl  28219  readdscl  28220  remulscl  28223  istrkg2ld  28257  istrkg3ld  28258  1loopgrvd2  29310  wwlksnextsurj  29704  isgrpo  30300  nmo  32281  reuxfrdf  32282  rexunirn  32283  dmrab  32288  disjorf  32362  fcoinvbr  32388  mpomptxf  32457  cnvoprabOLD  32496  fpwrelmapffslem  32508  ordtconnlem1  33519  ddemeas  33849  omssubaddlem  33913  omssubadd  33914  eulerpartlemgvv  33990  bnj89  34346  bnj133  34352  bnj1019  34404  bnj1101  34409  bnj1109  34411  bnj1143  34415  bnj1198  34420  bnj1304  34444  bnj605  34532  bnj607  34541  bnj600  34544  bnj865  34548  bnj916  34558  bnj983  34576  bnj985v  34578  bnj985  34579  bnj996  34581  bnj1033  34594  bnj1083  34603  bnj1090  34604  bnj1093  34605  bnj1110  34607  bnj1128  34615  bnj1145  34618  bnj1171  34625  bnj1172  34626  bnj1174  34628  bnj1176  34630  bnj1186  34632  bnj1189  34634  bnj1253  34642  bnj1279  34643  bnj1371  34654  bnj1374  34656  bnj1312  34683  exdifsn  34698  fineqvrep  34709  fineqvpow  34710  lfuhgr3  34723  loop1cycl  34741  satfvsucsuc  34969  satf0op  34981  axextprim  35289  axrepprim  35290  axunprim  35291  axpowprim  35292  axregprim  35293  axinfprim  35294  axacprim  35295  dftr6  35339  coep  35340  coepr  35341  dffr5  35342  cnvco1  35347  cnvco2  35348  eldm3  35349  fundmpss  35356  dfdm5  35362  dfrn5  35363  elima4  35365  axextdfeq  35387  19.12b  35391  axextndbi  35394  brtxp  35470  brpprod  35475  brsset  35479  dfon3  35482  brtxpsd  35484  elfix  35493  dffix2  35495  sscoid  35503  dffun10  35504  elfuns  35505  elsingles  35508  snelsingles  35512  dfiota3  35513  brimg  35527  brapply  35528  brcup  35529  brcap  35530  brsuccf  35531  funpartlem  35532  brrestrict  35539  dfrecs2  35540  dfrdg4  35541  neifg  35849  bj-equsexval  36130  bj-eeanvw  36184  bj-substw  36193  eliminable-abelv  36340  eliminable-abelab  36341  bj-denoteslem  36342  bj-rexvw  36352  bj-csbsnlem  36375  bj-gabima  36412  bj-snsetex  36436  bj-elsngl  36441  bj-snglc  36442  bj-abex  36503  bj-clex  36504  bj-clel3gALT  36521  bj-nul  36529  bj-dfid2ALT  36538  bj-restpw  36565  bj-restuni  36570  bj-dfmpoa  36591  bj-opabco  36661  bj-xpcossxp  36662  bj-imdirco  36663  mptsnunlem  36811  topdifinffinlem  36820  difunieq  36847  wl-dfclab  37057  poimirlem26  37113  ismblfin  37128  itg2addnclem3  37140  itg2addnc  37141  ismgmOLD  37317  sbcexfi  37584  sbccom2lem  37591  eldmres  37736  ecinn0  37819  ineleq  37820  moantr  37830  rnxrn  37864  rnxrnres  37865  dfcoss2  37879  dfcoss3  37880  cosscnv  37882  coss1cnvres  37883  coss2cnvepres  37884  1cossres  37895  cocossss  37902  rncossdmcoss  37921  eldmcoss2  37925  coss0  37945  cossid  37946  dfssr2  37965  eldmqs1cossres  38125  prtlem16  38335  prter2  38347  islshpat  38483  islpln5  39002  islvol5  39046  pmapglb  39237  polval2N  39373  cdlemftr3  40032  dibelval3  40614  dicelval3  40647  dihglb2  40809  sn-axrep5v  41698  prjspeclsp  42030  diophrex  42189  onsupmaxb  42661  nnoeomeqom  42735  tfsconcatlem  42759  tfsconcat0i  42768  rp-isfinite6  42942  snen1g  42948  relintab  43007  imaiun1  43075  coiun1  43076  clsk3nimkb  43464  expandexn  43720  ismnuprim  43725  rr-groth  43730  ismnushort  43732  rr-grothshortbi  43734  19.36vv  43814  19.37vv  43816  pm11.58  43821  pm11.6  43823  pm13.192  43841  2sbc5g  43847  iotasbc2  43851  onfrALTlem5  43975  onfrALTlem1  43981  ax6e2nd  43991  2sb5nd  43993  en3lplem2VD  44277  onfrALTlem5VD  44318  relopabVD  44334  ax6e2ndVD  44341  2sb5ndVD  44343  ax6e2ndALT  44363  2sb5ndALT  44365  rfcnnnub  44392  inn0f  44431  stoweidlem34  45416  stoweidlem35  45417  stoweidlem60  45442  smfpimcc  46190  ichexmpl1  46803  sprid  46808  dfgric2  47175  opeliun2xp  47390  eliunxp2  47391  mosssn2  47881  setrec1lem3  48114  elpglem3  48138  eximp-surprise  48211