Theorem exbii 1850

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

Syntax hints:   ↔ wb 206  ∃wex 1781

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

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

This theorem is referenced by:  2exbii  1851  3exbii  1852  exanali  1861  exancom  1863  19.43  1884  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistr  1956  exdistr2  1960  3exdistr  1962  19.12vvv  1996  excom13  2170  exrot4  2172  2sb5  2285  dfsb7  2286  eeor  2339  19.12vv  2352  eean  2353  eeeanv  2355  ee4anv  2356  ee4anvOLD  2357  2sb8ef  2361  equsexALT  2424  2sb5rf  2477  2sb8e  2535  mo4  2567  eu6lem  2574  sb8eulem  2599  cbvmovw  2603  cbvmow  2604  eu1  2611  sbmo  2615  2moswapv  2630  2moswap  2645  euae  2661  issettru  2815  issetlem  2817  clabel  2882  sbabel  2932  nabbib  3036  rextru  3069  rexbii2  3081  r2exlem  3127  r19.41v  3168  r3ex  3177  r19.41  3242  rexcom4  3265  2ex2rexrot  3273  rexv  3458  ceqsex2  3482  ceqsex2v  3483  ceqsex3v  3484  gencbvex  3488  spc3egv  3546  spc3gv  3547  ceqsrexv  3598  rexrab2  3647  euxfrw  3668  euxfr  3670  euind  3671  reu6  3673  reu3  3674  2reuswap  3693  2reuswap2  3694  reuind  3700  2reu5lem3  3704  2reu5  3705  2rmoswap  3708  sbcimdv  3798  sbcg  3802  sbccomlemOLD  3809  rmo2  3826  rmoanim  3833  rmoanimALT  3834  rexun  4137  reupick3  4271  euelss  4273  ndisj  4311  inn0f  4312  pssnel  4412  rexsns  4616  exsnrex  4625  snprc  4662  euabsn2  4670  reusn  4672  eusn  4675  elpreqpr  4811  elunirab  4866  uniprg  4867  uniun  4874  uniin  4875  uni0b  4877  uniintsn  4928  iuncom4  4943  dfiun2g  4973  iunn0  5010  iunxiun  5040  disjor  5068  cbvopab2  5162  cbvopab2v  5165  unopab  5166  axrep1  5213  axrep4v  5217  axrep4  5218  axrep4OLD  5219  axrep5  5220  axrep6  5221  axrep6OLD  5222  zfrep6  5224  zfrep4  5228  axsepgfromrep  5229  axnulALT  5239  0ex  5242  vnex  5251  inex1  5254  inuni  5287  axpweq  5288  zfpow  5303  axpow2  5304  vpwex  5314  zfpair  5358  zfpair2  5371  prex  5375  elOLD  5386  eqvinop  5435  copsexgw  5438  copsexg  5439  opabn0  5501  iunopab  5507  dfid2  5521  dfid3  5522  opeliunxp  5691  opeliun2xp  5692  xpiundi  5695  xpiundir  5696  elvvv  5700  csbxp  5725  eliunxp  5786  exopxfr  5792  relop  5799  opelco2g  5816  cnvco  5834  cnvuni  5835  dfdm3  5836  dfrn2  5837  dfrn3  5838  elrng  5840  dfdm4  5844  csbdm  5846  eldm2g  5848  dmun  5859  dmin  5860  dmiun  5862  dmuni  5863  dmopab  5864  dmi  5870  dmep  5872  rnep  5876  dmxp  5878  rnopab  5903  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  dmres  5971  elsnres  5980  dfima2  6021  elima3  6026  imadmrn  6029  imai  6033  args  6051  rniun  6105  xpdifid  6126  ssrnres  6136  dmsnn0  6165  dmsnopg  6171  cnvresima  6188  mptpreima  6196  dfco2  6203  coundi  6205  coundir  6206  resco  6208  imaco  6209  rnco  6210  rncoOLD  6211  coiun  6215  coi1  6221  coass  6224  xpco  6247  elsnxp  6249  dfpo2  6254  dffun5  6506  imadif  6576  tz6.12-2  6821  brprcneu  6824  brprcneuALT  6825  dffv2  6929  fndmin  6991  fvn0ssdmfun  7020  abrexco  7192  imaiun  7193  isomin  7285  imaeqsexvOLD  7311  dfoprab2  7418  cbvoprab2  7448  zfun  7683  uniex2  7685  uniuni  7709  elxp4  7866  elxp5  7867  fiun  7889  f1iun  7890  f11o  7893  fvresex  7906  opabex3d  7911  opabex3rd  7912  opabex3  7913  abexssex  7916  abexex  7917  oprabrexex2  7924  releldm2  7989  dfopab2  7998  dfoprab3s  7999  fsplit  8060  frxp  8069  suppvalbr  8107  cnvimadfsn  8115  brtpos2  8175  dfrecs3  8305  oarec  8490  oeeu  8532  domen  8901  xpsnen  8992  xpcomco  8998  xpassen  9002  inf2  9535  zfinf  9551  axinf2  9552  zfinf2  9554  brttrcl2  9626  ttrcltr  9628  ttrclresv  9629  ttrclselem2  9638  rankuni  9778  scott0  9801  cp  9806  ween  9948  aceq1  10030  aceq0  10031  aceq2  10032  dfac5lem1  10036  dfac5lem2  10037  dfac5lem3  10038  kmlem3  10066  kmlem14  10077  kmlem15  10078  kmlem16  10079  cflem  10158  cflemOLD  10159  cf0  10164  cfval2  10173  cfss  10178  cfslb  10179  fin23lem32  10257  axdc2lem  10361  zfac  10373  ac9  10396  ac9s  10406  axpowndlem3  10513  zfcndrep  10528  zfcndun  10529  zfcndpow  10530  zfcndinf  10532  zfcndac  10533  axgroth5  10738  axgroth2  10739  axgroth6  10742  axgroth3  10745  axgroth4  10746  grothprim  10748  grothtsk  10749  genpass  10923  ltexprlem1  10950  ltexprlem4  10953  supaddc  12114  supadd  12115  supmul1  12116  supmullem2  12118  2rexuz  12841  nnwos  12856  hashgt23el  14377  hashfun  14390  wwlktovfo  14911  xpcogend  14927  cbvsum  15648  cbvsumv  15649  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  iprodmul  15959  maxprmfct  16670  4sqlem12  16918  vdwmc  16940  cshwrepswhash1  17064  imasleval  17496  isacs2  17610  cicsym  17762  gsumval3eu  19870  lidlnz  21232  isbasis2g  22923  tgval2  22931  ntreq0  23052  lmff  23276  cmpfi  23383  is1stc2  23417  1stcelcls  23436  unisngl  23502  isfbas2  23810  elfg  23846  alexsubALTlem3  24024  ustfilxp  24188  metrest  24499  metuel2  24540  restmetu  24545  dchrvmasumlema  27477  elold  27865  lrrecfr  27949  leadds1  27995  addsuniflem  28007  addsasslem1  28009  addsasslem2  28010  mulsuniflem  28155  addsdilem1  28157  addsdilem2  28158  mulsasslem1  28169  mulsasslem2  28170  elreno2  28501  renegscl  28504  readdscl  28505  remulscl  28508  istrkg2ld  28542  istrkg3ld  28543  1loopgrvd2  29587  wwlksnextsurj  29983  isgrpo  30583  nmo  32574  reuxfrdf  32575  rexunirn  32576  dmrab  32581  disjorf  32664  fcoinvbr  32690  mpomptxf  32766  fpwrelmapffslem  32820  1arithidom  33612  ordtconnlem1  34084  ddemeas  34396  omssubaddlem  34459  omssubadd  34460  eulerpartlemgvv  34536  bnj89  34880  bnj133  34886  bnj1019  34938  bnj1101  34943  bnj1109  34945  bnj1143  34948  bnj1198  34953  bnj1304  34977  bnj605  35065  bnj607  35074  bnj600  35077  bnj865  35081  bnj916  35091  bnj983  35109  bnj985v  35111  bnj985  35112  bnj996  35114  bnj1033  35127  bnj1083  35136  bnj1090  35137  bnj1093  35138  bnj1110  35140  bnj1128  35148  bnj1145  35151  bnj1171  35158  bnj1172  35159  bnj1174  35161  bnj1176  35163  bnj1186  35165  bnj1189  35167  bnj1253  35175  bnj1279  35176  bnj1371  35187  bnj1374  35189  bnj1312  35216  exdifsn  35237  axnulALT2  35240  axprALT2  35269  fineqvrep  35274  fineqvpow  35275  axreg  35287  axregscl  35288  axregs  35299  lfuhgr3  35318  loop1cycl  35335  satfvsucsuc  35563  satf0op  35575  axextprim  35899  axrepprim  35900  axunprim  35901  axpowprim  35902  axregprim  35903  axinfprim  35904  axacprim  35905  dftr6  35949  coep  35950  coepr  35951  dffr5  35952  cnvco1  35957  cnvco2  35958  eldm3  35959  fundmpss  35965  dfdm5  35971  dfrn5  35972  elima4  35974  axextdfeq  35993  19.12b  35997  axextndbi  36000  brtxp  36076  brpprod  36081  brsset  36085  dfon3  36088  brtxpsd  36090  elfix  36099  dffix2  36101  sscoid  36109  dffun10  36110  elfuns  36111  elsingles  36114  snelsingles  36118  dfiota3  36119  brimg  36133  brapply  36134  brcup  36135  brcap  36136  lemsuccf  36137  funpartlem  36140  brrestrict  36147  dfrecs2  36148  dfrdg4  36149  sumeq2si  36400  prodeq2si  36402  cbvoprab2vw  36436  cbvoprab23vw  36438  cbvprodvw2  36445  neifg  36569  regsfromregtco  36736  regsfromunir1  36738  mh-prprimbi  36741  mh-unprimbi  36742  mh-infprim1bi  36744  mh-infprim2bi  36745  mh-infprim3bi  36746  bj-df-sb  36960  bj-dfsbc  36962  bj-equsexval  36970  bj-eeanvw  37028  bj-substw  37038  eliminable-abelv  37192  eliminable-abelab  37193  bj-denoteslem  37194  bj-rexvw  37203  bj-csbsnlem  37226  bj-gabima  37263  bj-snsetex  37286  bj-elsngl  37291  bj-snglc  37292  bj-abex  37353  bj-clex  37354  bj-clel3gALT  37371  bj-nul  37379  bj-dfid2ALT  37388  bj-rep  37396  bj-axseprep  37397  bj-restpw  37420  bj-restuni  37425  bj-dfmpoa  37446  bj-opabco  37518  bj-xpcossxp  37519  bj-imdirco  37520  mptsnunlem  37668  topdifinffinlem  37677  difunieq  37704  wl-dfclab  37924  poimirlem26  37981  ismblfin  37996  itg2addnclem3  38008  itg2addnc  38009  ismgmOLD  38185  sbcexfi  38452  sbccom2lem  38459  eldmres  38612  ecinn0  38688  ineleq  38689  moantr  38707  dmcnvep  38723  rnxrn  38756  rnxrnres  38757  dmsucmap  38803  dfcoss2  38838  dfcoss3  38839  cosscnv  38841  coss1cnvres  38842  coss2cnvepres  38843  1cossres  38854  cocossss  38861  rncossdmcoss  38880  eldmcoss2  38884  coss0  38904  cossid  38905  dfssr2  38914  eldmqs1cossres  39079  prtlem16  39329  prter2  39341  islshpat  39477  islpln5  39995  islvol5  40039  pmapglb  40230  polval2N  40366  cdlemftr3  41025  dibelval3  41607  dicelval3  41640  dihglb2  41802  sn-axrep5v  42672  prjspeclsp  43059  euabsn2w  43126  diophrex  43221  onsupmaxb  43685  nnoeomeqom  43758  tfsconcatlem  43782  tfsconcat0i  43791  rp-isfinite6  43963  snen1g  43969  relintab  44028  imaiun1  44096  coiun1  44097  clsk3nimkb  44485  expandexn  44734  ismnuprim  44739  rr-groth  44744  ismnushort  44746  rr-grothshortbi  44748  19.36vv  44828  19.37vv  44830  pm11.58  44835  pm11.6  44837  pm13.192  44855  2sbc5g  44861  iotasbc2  44865  onfrALTlem5  44987  onfrALTlem1  44993  ax6e2nd  45003  2sb5nd  45005  en3lplem2VD  45288  onfrALTlem5VD  45329  relopabVD  45345  ax6e2ndVD  45352  2sb5ndVD  45354  ax6e2ndALT  45374  2sb5ndALT  45376  dfac5prim  45435  brpermmodel  45448  permaxrep  45451  permac8prim  45459  rfcnnnub  45485  stoweidlem34  46480  stoweidlem35  46481  stoweidlem60  46506  smfpimcc  47254  ichexmpl1  47941  sprid  47946  dfgric2  48403  usgrgrtrirex  48438  grlimgrtri  48491  eliunxp2  48822  mosssn2  49304  coxp  49320  istermc  49961  setrec1lem3  50176  elpglem3  50200  eximp-surprise  50271