Theorem exbii 1848

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

Syntax hints:   ↔ wb 206  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  2exbii  1849  3exbii  1850  exanali  1859  exancom  1861  19.43  1882  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1954  exdistr2  1958  3exdistr  1960  19.12vvv  1988  excom13  2164  exrot4  2166  2sb5  2278  dfsb7  2279  eeor  2335  eeorOLD  2336  19.12vv  2349  eean  2350  eeeanv  2352  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2359  equsexALT  2424  2sb5rf  2477  2sb8e  2535  mo4  2566  eu6lem  2573  eubii  2585  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  eu1  2610  sbmo  2614  2moswapv  2629  2moswap  2644  euae  2660  issettru  2819  issetlem  2821  clabel  2888  sbabel  2938  sbabelOLD  2939  nabbib  3045  rextru  3077  rexbii2  3090  r2exlem  3143  r19.41v  3189  r3ex  3198  r19.41  3263  rexcom4  3288  rexcomOLD  3291  2ex2rexrot  3298  rexv  3509  cgsex4gOLD  3529  ceqsex2  3535  ceqsex2v  3536  ceqsex3v  3537  gencbvex  3541  spc3egv  3603  spc3gv  3604  ceqsrexv  3655  rexabOLD  3701  rexrab2  3706  euxfrw  3727  euxfr  3729  euind  3730  reu6  3732  reu3  3733  2reuswap  3752  2reuswap2  3753  reuind  3759  2reu5lem3  3763  2reu5  3764  2rmoswap  3767  sbcimdv  3859  sbcg  3863  sbccomlemOLD  3870  rmo2  3887  rmoanim  3894  rmoanimALT  3895  rexun  4196  reupick3  4330  euelss  4332  ndisj  4370  inn0f  4371  pssnel  4471  rexsns  4671  exsnrex  4680  snprc  4717  euabsn2  4725  reusn  4727  eusn  4730  elpreqpr  4867  elunirab  4922  uniprg  4923  uniun  4930  uniin  4931  uni0b  4933  uniintsn  4985  iuncom4  5000  dfiun2g  5030  dfiun2gOLD  5031  iunn0  5067  iunxiun  5097  disjor  5125  cbvopab2  5219  cbvopab2v  5223  unopab  5224  axrep1  5280  axrep4v  5284  axrep4  5285  axrep4OLD  5286  axrep5  5287  axrep6  5288  axrep6OLD  5289  zfrep4  5293  axsepgfromrep  5294  axnulALT  5304  0ex  5307  vnex  5314  inex1  5317  inuni  5350  axpweq  5351  zfpow  5366  axpow2  5367  vpwex  5377  zfpair  5421  zfpair2  5433  el  5442  eqvinop  5492  copsexgw  5495  copsexg  5496  opabn0  5558  iunopab  5564  iunopabOLD  5565  dfid2  5580  dfid3  5581  opeliunxp  5752  opeliun2xp  5753  xpiundi  5756  xpiundir  5757  elvvv  5761  csbxp  5785  eliunxp  5848  exopxfr  5854  relop  5861  opelco2g  5878  cnvco  5896  cnvuni  5897  dfdm3  5898  dfrn2  5899  dfrn3  5900  elrng  5902  dfdm4  5906  csbdm  5908  eldm2g  5910  dmun  5921  dmin  5922  dmiun  5924  dmuni  5925  dmopab  5926  dmi  5932  dmep  5934  rnep  5937  dmxp  5939  rnopab  5965  dmcosseq  5987  dmcosseqOLD  5988  dmres  6030  elsnres  6039  dfima2  6080  elima3  6085  imadmrn  6088  imai  6092  args  6110  rniun  6167  xpdifid  6188  ssrnres  6198  dmsnn0  6227  dmsnopg  6233  cnvresima  6250  mptpreima  6258  dfco2  6265  coundi  6267  coundir  6268  resco  6270  imaco  6271  rnco  6272  coiun  6276  coi1  6282  coass  6285  xpco  6309  elsnxp  6311  dfpo2  6316  dffun2OLDOLD  6573  dffun5  6578  imadif  6650  funimaexgOLD  6654  brprcneu  6896  brprcneuALT  6897  dffv2  7004  fndmin  7065  fvn0ssdmfun  7094  abrexco  7264  imaiun  7265  isomin  7357  imaeqsexvOLD  7383  dfoprab2  7491  cbvoprab2  7521  zfun  7756  uniex2  7758  uniuni  7782  elxp4  7944  elxp5  7945  fiun  7967  f1iun  7968  f11o  7971  fvresex  7984  opabex3d  7990  opabex3rd  7991  opabex3  7992  abexssex  7995  abexex  7996  oprabrexex2  8003  releldm2  8068  dfopab2  8077  dfoprab3s  8078  fsplit  8142  frxp  8151  suppvalbr  8189  cnvimadfsn  8197  brtpos2  8257  dfwrecsOLD  8338  wfrfunOLD  8359  dfrecs3  8412  dfrecs3OLD  8413  oarec  8600  oeeu  8641  domen  9002  xpsnen  9095  xpcomco  9102  xpassen  9106  dif1enOLD  9202  inf2  9663  zfinf  9679  axinf2  9680  zfinf2  9682  brttrcl2  9754  ttrcltr  9756  ttrclresv  9757  ttrclselem2  9766  rankuni  9903  scott0  9926  cp  9931  ween  10075  aceq1  10157  aceq0  10158  aceq2  10159  dfac5lem1  10163  dfac5lem2  10164  dfac5lem3  10165  kmlem3  10193  kmlem14  10204  kmlem15  10205  kmlem16  10206  cflem  10285  cflemOLD  10286  cf0  10291  cfval2  10300  cfss  10305  cfslb  10306  fin23lem32  10384  axdc2lem  10488  zfac  10500  ac9  10523  ac9s  10533  axpowndlem3  10639  zfcndrep  10654  zfcndun  10655  zfcndpow  10656  zfcndinf  10658  zfcndac  10659  axgroth5  10864  axgroth2  10865  axgroth6  10868  axgroth3  10871  axgroth4  10872  grothprim  10874  grothtsk  10875  genpass  11049  ltexprlem1  11076  ltexprlem4  11079  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  2rexuz  12942  nnwos  12957  hashgt23el  14463  hashfun  14476  wwlktovfo  14997  xpcogend  15013  cbvsum  15731  cbvsumv  15732  cbvprod  15949  cbvprodv  15950  prodeq1i  15952  iprodmul  16039  maxprmfct  16746  4sqlem12  16994  vdwmc  17016  cshwrepswhash1  17140  imasleval  17586  isacs2  17696  cicsym  17848  gsumval3eu  19922  lidlnz  21252  isbasis2g  22955  tgval2  22963  ntreq0  23085  lmff  23309  cmpfi  23416  is1stc2  23450  1stcelcls  23469  unisngl  23535  isfbas2  23843  elfg  23879  alexsubALTlem3  24057  ustfilxp  24221  metrest  24537  metuel2  24578  restmetu  24583  dchrvmasumlema  27544  elold  27908  lrrecfr  27976  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  mulsuniflem  28175  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  renegscl  28430  readdscl  28431  remulscl  28434  istrkg2ld  28468  istrkg3ld  28469  1loopgrvd2  29521  wwlksnextsurj  29920  isgrpo  30516  nmo  32509  reuxfrdf  32510  rexunirn  32511  dmrab  32516  disjorf  32592  fcoinvbr  32618  mpomptxf  32687  fpwrelmapffslem  32743  1arithidom  33565  ordtconnlem1  33923  ddemeas  34237  omssubaddlem  34301  omssubadd  34302  eulerpartlemgvv  34378  bnj89  34735  bnj133  34741  bnj1019  34793  bnj1101  34798  bnj1109  34800  bnj1143  34804  bnj1198  34809  bnj1304  34833  bnj605  34921  bnj607  34930  bnj600  34933  bnj865  34937  bnj916  34947  bnj983  34965  bnj985v  34967  bnj985  34968  bnj996  34970  bnj1033  34983  bnj1083  34992  bnj1090  34993  bnj1093  34994  bnj1110  34996  bnj1128  35004  bnj1145  35007  bnj1171  35014  bnj1172  35015  bnj1174  35017  bnj1176  35019  bnj1186  35021  bnj1189  35023  bnj1253  35031  bnj1279  35032  bnj1371  35043  bnj1374  35045  bnj1312  35072  exdifsn  35093  fineqvrep  35109  fineqvpow  35110  lfuhgr3  35125  loop1cycl  35142  satfvsucsuc  35370  satf0op  35382  axextprim  35701  axrepprim  35702  axunprim  35703  axpowprim  35704  axregprim  35705  axinfprim  35706  axacprim  35707  dftr6  35751  coep  35752  coepr  35753  dffr5  35754  cnvco1  35759  cnvco2  35760  eldm3  35761  fundmpss  35767  dfdm5  35773  dfrn5  35774  elima4  35776  axextdfeq  35798  19.12b  35802  axextndbi  35805  brtxp  35881  brpprod  35886  brsset  35890  dfon3  35893  brtxpsd  35895  elfix  35904  dffix2  35906  sscoid  35914  dffun10  35915  elfuns  35916  elsingles  35919  snelsingles  35923  dfiota3  35924  brimg  35938  brapply  35939  brcup  35940  brcap  35941  brsuccf  35942  funpartlem  35943  brrestrict  35950  dfrecs2  35951  dfrdg4  35952  sumeq2si  36203  prodeq2si  36205  cbvoprab2vw  36239  cbvoprab23vw  36241  cbvprodvw2  36248  neifg  36372  bj-equsexval  36661  bj-eeanvw  36714  bj-substw  36723  eliminable-abelv  36870  eliminable-abelab  36871  bj-denoteslem  36872  bj-rexvw  36881  bj-csbsnlem  36904  bj-gabima  36941  bj-snsetex  36964  bj-elsngl  36969  bj-snglc  36970  bj-abex  37031  bj-clex  37032  bj-clel3gALT  37049  bj-nul  37057  bj-dfid2ALT  37066  bj-restpw  37093  bj-restuni  37098  bj-dfmpoa  37119  bj-opabco  37189  bj-xpcossxp  37190  bj-imdirco  37191  mptsnunlem  37339  topdifinffinlem  37348  difunieq  37375  wl-dfclab  37597  poimirlem26  37653  ismblfin  37668  itg2addnclem3  37680  itg2addnc  37681  ismgmOLD  37857  sbcexfi  38124  sbccom2lem  38131  eldmres  38271  ecinn0  38354  ineleq  38355  moantr  38365  rnxrn  38399  rnxrnres  38400  dfcoss2  38414  dfcoss3  38415  cosscnv  38417  coss1cnvres  38418  coss2cnvepres  38419  1cossres  38430  cocossss  38437  rncossdmcoss  38456  eldmcoss2  38460  coss0  38480  cossid  38481  dfssr2  38500  eldmqs1cossres  38660  prtlem16  38870  prter2  38882  islshpat  39018  islpln5  39537  islvol5  39581  pmapglb  39772  polval2N  39908  cdlemftr3  40567  dibelval3  41149  dicelval3  41182  dihglb2  41344  sn-axrep5v  42255  prjspeclsp  42622  euabsn2w  42689  diophrex  42786  onsupmaxb  43251  nnoeomeqom  43325  tfsconcatlem  43349  tfsconcat0i  43358  rp-isfinite6  43531  snen1g  43537  relintab  43596  imaiun1  43664  coiun1  43665  clsk3nimkb  44053  expandexn  44308  ismnuprim  44313  rr-groth  44318  ismnushort  44320  rr-grothshortbi  44322  19.36vv  44402  19.37vv  44404  pm11.58  44409  pm11.6  44411  pm13.192  44429  2sbc5g  44435  iotasbc2  44439  onfrALTlem5  44562  onfrALTlem1  44568  ax6e2nd  44578  2sb5nd  44580  en3lplem2VD  44864  onfrALTlem5VD  44905  relopabVD  44921  ax6e2ndVD  44928  2sb5ndVD  44930  ax6e2ndALT  44950  2sb5ndALT  44952  dfac5prim  45007  rfcnnnub  45041  stoweidlem34  46049  stoweidlem35  46050  stoweidlem60  46075  smfpimcc  46823  ichexmpl1  47456  sprid  47461  dfgric2  47884  usgrgrtrirex  47917  grlimgrtri  47963  eliunxp2  48250  mosssn2  48736  coxp  48744  istermc  49121  setrec1lem3  49208  elpglem3  49232  eximp-surprise  49303