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  1994  excom13  2165  exrot4  2167  2sb5  2278  dfsb7  2279  eeor  2332  19.12vv  2345  eean  2346  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  equsexALT  2417  2sb5rf  2470  2sb8e  2528  mo4  2559  eu6lem  2566  eubii  2578  sb8eulem  2591  cbvmovw  2595  cbvmow  2596  eu1  2603  sbmo  2607  2moswapv  2622  2moswap  2637  euae  2653  issettru  2806  issetlem  2808  clabel  2874  sbabel  2924  nabbib  3028  rextru  3060  rexbii2  3072  r2exlem  3122  r19.41v  3165  r3ex  3174  r19.41  3239  rexcom4  3262  2ex2rexrot  3271  rexv  3472  cgsex4gOLD  3492  ceqsex2  3498  ceqsex2v  3499  ceqsex3v  3500  gencbvex  3504  spc3egv  3566  spc3gv  3567  ceqsrexv  3618  rexrab2  3668  euxfrw  3689  euxfr  3691  euind  3692  reu6  3694  reu3  3695  2reuswap  3714  2reuswap2  3715  reuind  3721  2reu5lem3  3725  2reu5  3726  2rmoswap  3729  sbcimdv  3819  sbcg  3823  sbccomlemOLD  3830  rmo2  3847  rmoanim  3854  rmoanimALT  3855  rexun  4155  reupick3  4289  euelss  4291  ndisj  4329  inn0f  4330  pssnel  4430  rexsns  4631  exsnrex  4640  snprc  4677  euabsn2  4685  reusn  4687  eusn  4690  elpreqpr  4827  elunirab  4882  uniprg  4883  uniun  4890  uniin  4891  uni0b  4893  uniintsn  4945  iuncom4  4960  dfiun2g  4990  iunn0  5026  iunxiun  5056  disjor  5084  cbvopab2  5178  cbvopab2v  5181  unopab  5182  axrep1  5230  axrep4v  5234  axrep4  5235  axrep4OLD  5236  axrep5  5237  axrep6  5238  axrep6OLD  5239  zfrep4  5243  axsepgfromrep  5244  axnulALT  5254  0ex  5257  vnex  5264  inex1  5267  inuni  5300  axpweq  5301  zfpow  5316  axpow2  5317  vpwex  5327  zfpair  5371  zfpair2  5383  el  5392  eqvinop  5442  copsexgw  5445  copsexg  5446  opabn0  5508  iunopab  5514  dfid2  5528  dfid3  5529  opeliunxp  5698  opeliun2xp  5699  xpiundi  5702  xpiundir  5703  elvvv  5707  csbxp  5730  eliunxp  5791  exopxfr  5797  relop  5804  opelco2g  5821  cnvco  5839  cnvuni  5840  dfdm3  5841  dfrn2  5842  dfrn3  5843  elrng  5845  dfdm4  5849  csbdm  5851  eldm2g  5853  dmun  5864  dmin  5865  dmiun  5867  dmuni  5868  dmopab  5869  dmi  5875  dmep  5877  rnep  5880  dmxp  5882  rnopab  5907  dmcosseq  5929  dmcosseqOLD  5930  dmres  5972  elsnres  5981  dfima2  6022  elima3  6027  imadmrn  6030  imai  6034  args  6052  rniun  6108  xpdifid  6129  ssrnres  6139  dmsnn0  6168  dmsnopg  6174  cnvresima  6191  mptpreima  6199  dfco2  6206  coundi  6208  coundir  6209  resco  6211  imaco  6212  rnco  6213  coiun  6217  coi1  6223  coass  6226  xpco  6250  elsnxp  6252  dfpo2  6257  dffun5  6514  imadif  6584  brprcneu  6830  brprcneuALT  6831  dffv2  6938  fndmin  6999  fvn0ssdmfun  7028  abrexco  7200  imaiun  7201  isomin  7294  imaeqsexvOLD  7320  dfoprab2  7427  cbvoprab2  7457  zfun  7692  uniex2  7694  uniuni  7718  elxp4  7878  elxp5  7879  fiun  7901  f1iun  7902  f11o  7905  fvresex  7918  opabex3d  7923  opabex3rd  7924  opabex3  7925  abexssex  7928  abexex  7929  oprabrexex2  7936  releldm2  8001  dfopab2  8010  dfoprab3s  8011  fsplit  8073  frxp  8082  suppvalbr  8120  cnvimadfsn  8128  brtpos2  8188  dfrecs3  8318  oarec  8503  oeeu  8544  domen  8910  xpsnen  9002  xpcomco  9008  xpassen  9012  dif1enOLD  9103  inf2  9552  zfinf  9568  axinf2  9569  zfinf2  9571  brttrcl2  9643  ttrcltr  9645  ttrclresv  9646  ttrclselem2  9655  rankuni  9792  scott0  9815  cp  9820  ween  9964  aceq1  10046  aceq0  10047  aceq2  10048  dfac5lem1  10052  dfac5lem2  10053  dfac5lem3  10054  kmlem3  10082  kmlem14  10093  kmlem15  10094  kmlem16  10095  cflem  10174  cflemOLD  10175  cf0  10180  cfval2  10189  cfss  10194  cfslb  10195  fin23lem32  10273  axdc2lem  10377  zfac  10389  ac9  10412  ac9s  10422  axpowndlem3  10528  zfcndrep  10543  zfcndun  10544  zfcndpow  10545  zfcndinf  10547  zfcndac  10548  axgroth5  10753  axgroth2  10754  axgroth6  10757  axgroth3  10760  axgroth4  10761  grothprim  10763  grothtsk  10764  genpass  10938  ltexprlem1  10965  ltexprlem4  10968  supaddc  12126  supadd  12127  supmul1  12128  supmullem2  12130  2rexuz  12835  nnwos  12850  hashgt23el  14365  hashfun  14378  wwlktovfo  14900  xpcogend  14916  cbvsum  15637  cbvsumv  15638  cbvprod  15855  cbvprodv  15856  prodeq1i  15858  iprodmul  15945  maxprmfct  16655  4sqlem12  16903  vdwmc  16925  cshwrepswhash1  17049  imasleval  17480  isacs2  17590  cicsym  17742  gsumval3eu  19810  lidlnz  21128  isbasis2g  22811  tgval2  22819  ntreq0  22940  lmff  23164  cmpfi  23271  is1stc2  23305  1stcelcls  23324  unisngl  23390  isfbas2  23698  elfg  23734  alexsubALTlem3  23912  ustfilxp  24076  metrest  24388  metuel2  24429  restmetu  24434  dchrvmasumlema  27387  elold  27757  lrrecfr  27826  sleadd1  27872  addsuniflem  27884  addsasslem1  27886  addsasslem2  27887  mulsuniflem  28028  addsdilem1  28030  addsdilem2  28031  mulsasslem1  28042  mulsasslem2  28043  renegscl  28325  readdscl  28326  remulscl  28329  istrkg2ld  28363  istrkg3ld  28364  1loopgrvd2  29407  wwlksnextsurj  29803  isgrpo  30399  nmo  32392  reuxfrdf  32393  rexunirn  32394  dmrab  32399  disjorf  32481  fcoinvbr  32507  mpomptxf  32574  fpwrelmapffslem  32628  1arithidom  33481  ordtconnlem1  33887  ddemeas  34199  omssubaddlem  34263  omssubadd  34264  eulerpartlemgvv  34340  bnj89  34684  bnj133  34690  bnj1019  34742  bnj1101  34747  bnj1109  34749  bnj1143  34753  bnj1198  34758  bnj1304  34782  bnj605  34870  bnj607  34879  bnj600  34882  bnj865  34886  bnj916  34896  bnj983  34914  bnj985v  34916  bnj985  34917  bnj996  34919  bnj1033  34932  bnj1083  34941  bnj1090  34942  bnj1093  34943  bnj1110  34945  bnj1128  34953  bnj1145  34956  bnj1171  34963  bnj1172  34964  bnj1174  34966  bnj1176  34968  bnj1186  34970  bnj1189  34972  bnj1253  34980  bnj1279  34981  bnj1371  34992  bnj1374  34994  bnj1312  35021  exdifsn  35042  fineqvrep  35058  fineqvpow  35059  lfuhgr3  35080  loop1cycl  35097  satfvsucsuc  35325  satf0op  35337  axextprim  35661  axrepprim  35662  axunprim  35663  axpowprim  35664  axregprim  35665  axinfprim  35666  axacprim  35667  dftr6  35711  coep  35712  coepr  35713  dffr5  35714  cnvco1  35719  cnvco2  35720  eldm3  35721  fundmpss  35727  dfdm5  35733  dfrn5  35734  elima4  35736  axextdfeq  35758  19.12b  35762  axextndbi  35765  brtxp  35841  brpprod  35846  brsset  35850  dfon3  35853  brtxpsd  35855  elfix  35864  dffix2  35866  sscoid  35874  dffun10  35875  elfuns  35876  elsingles  35879  snelsingles  35883  dfiota3  35884  brimg  35898  brapply  35899  brcup  35900  brcap  35901  brsuccf  35902  funpartlem  35903  brrestrict  35910  dfrecs2  35911  dfrdg4  35912  sumeq2si  36163  prodeq2si  36165  cbvoprab2vw  36199  cbvoprab23vw  36201  cbvprodvw2  36208  neifg  36332  bj-equsexval  36621  bj-eeanvw  36674  bj-substw  36683  eliminable-abelv  36830  eliminable-abelab  36831  bj-denoteslem  36832  bj-rexvw  36841  bj-csbsnlem  36864  bj-gabima  36901  bj-snsetex  36924  bj-elsngl  36929  bj-snglc  36930  bj-abex  36991  bj-clex  36992  bj-clel3gALT  37009  bj-nul  37017  bj-dfid2ALT  37026  bj-restpw  37053  bj-restuni  37058  bj-dfmpoa  37079  bj-opabco  37149  bj-xpcossxp  37150  bj-imdirco  37151  mptsnunlem  37299  topdifinffinlem  37308  difunieq  37335  wl-dfclab  37557  poimirlem26  37613  ismblfin  37628  itg2addnclem3  37640  itg2addnc  37641  ismgmOLD  37817  sbcexfi  38084  sbccom2lem  38091  eldmres  38232  ecinn0  38308  ineleq  38309  moantr  38319  dmcnvep  38334  rnxrn  38357  rnxrnres  38358  dfcoss2  38377  dfcoss3  38378  cosscnv  38380  coss1cnvres  38381  coss2cnvepres  38382  1cossres  38393  cocossss  38400  rncossdmcoss  38419  eldmcoss2  38423  coss0  38443  cossid  38444  dfssr2  38463  eldmqs1cossres  38624  prtlem16  38835  prter2  38847  islshpat  38983  islpln5  39502  islvol5  39546  pmapglb  39737  polval2N  39873  cdlemftr3  40532  dibelval3  41114  dicelval3  41147  dihglb2  41309  sn-axrep5v  42177  prjspeclsp  42573  euabsn2w  42640  diophrex  42736  onsupmaxb  43201  nnoeomeqom  43274  tfsconcatlem  43298  tfsconcat0i  43307  rp-isfinite6  43480  snen1g  43486  relintab  43545  imaiun1  43613  coiun1  43614  clsk3nimkb  44002  expandexn  44251  ismnuprim  44256  rr-groth  44261  ismnushort  44263  rr-grothshortbi  44265  19.36vv  44345  19.37vv  44347  pm11.58  44352  pm11.6  44354  pm13.192  44372  2sbc5g  44378  iotasbc2  44382  onfrALTlem5  44505  onfrALTlem1  44511  ax6e2nd  44521  2sb5nd  44523  en3lplem2VD  44806  onfrALTlem5VD  44847  relopabVD  44863  ax6e2ndVD  44870  2sb5ndVD  44872  ax6e2ndALT  44892  2sb5ndALT  44894  dfac5prim  44953  brpermmodel  44966  permaxrep  44969  permac8prim  44977  rfcnnnub  45003  stoweidlem34  46005  stoweidlem35  46006  stoweidlem60  46031  smfpimcc  46779  ichexmpl1  47443  sprid  47448  dfgric2  47888  usgrgrtrirex  47922  grlimgrtri  47968  eliunxp2  48295  mosssn2  48778  coxp  48794  istermc  49436  setrec1lem3  49651  elpglem3  49675  eximp-surprise  49746