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  2334  eeorOLD  2335  19.12vv  2348  eean  2349  eeeanv  2351  ee4anv  2352  ee4anvOLD  2353  2sb8ef  2358  equsexALT  2423  2sb5rf  2476  2sb8e  2534  mo4  2565  eu6lem  2572  eubii  2584  sb8eulem  2597  cbvmovw  2601  cbvmow  2602  eu1  2609  sbmo  2613  2moswapv  2628  2moswap  2643  euae  2659  issettru  2812  issetlem  2814  clabel  2881  sbabel  2931  nabbib  3035  rextru  3067  rexbii2  3079  r2exlem  3129  r19.41v  3174  r3ex  3183  r19.41  3246  rexcom4  3269  rexcomOLD  3272  2ex2rexrot  3279  rexv  3488  cgsex4gOLD  3508  ceqsex2  3514  ceqsex2v  3515  ceqsex3v  3516  gencbvex  3520  spc3egv  3582  spc3gv  3583  ceqsrexv  3634  rexrab2  3683  euxfrw  3704  euxfr  3706  euind  3707  reu6  3709  reu3  3710  2reuswap  3729  2reuswap2  3730  reuind  3736  2reu5lem3  3740  2reu5  3741  2rmoswap  3744  sbcimdv  3834  sbcg  3838  sbccomlemOLD  3845  rmo2  3862  rmoanim  3869  rmoanimALT  3870  rexun  4171  reupick3  4305  euelss  4307  ndisj  4345  inn0f  4346  pssnel  4446  rexsns  4647  exsnrex  4656  snprc  4693  euabsn2  4701  reusn  4703  eusn  4706  elpreqpr  4843  elunirab  4898  uniprg  4899  uniun  4906  uniin  4907  uni0b  4909  uniintsn  4961  iuncom4  4976  dfiun2g  5006  dfiun2gOLD  5007  iunn0  5043  iunxiun  5073  disjor  5101  cbvopab2  5195  cbvopab2v  5199  unopab  5200  axrep1  5250  axrep4v  5254  axrep4  5255  axrep4OLD  5256  axrep5  5257  axrep6  5258  axrep6OLD  5259  zfrep4  5263  axsepgfromrep  5264  axnulALT  5274  0ex  5277  vnex  5284  inex1  5287  inuni  5320  axpweq  5321  zfpow  5336  axpow2  5337  vpwex  5347  zfpair  5391  zfpair2  5403  el  5412  eqvinop  5462  copsexgw  5465  copsexg  5466  opabn0  5528  iunopab  5534  iunopabOLD  5535  dfid2  5550  dfid3  5551  opeliunxp  5721  opeliun2xp  5722  xpiundi  5725  xpiundir  5726  elvvv  5730  csbxp  5754  eliunxp  5817  exopxfr  5823  relop  5830  opelco2g  5847  cnvco  5865  cnvuni  5866  dfdm3  5867  dfrn2  5868  dfrn3  5869  elrng  5871  dfdm4  5875  csbdm  5877  eldm2g  5879  dmun  5890  dmin  5891  dmiun  5893  dmuni  5894  dmopab  5895  dmi  5901  dmep  5903  rnep  5906  dmxp  5908  rnopab  5934  dmcosseq  5956  dmcosseqOLD  5957  dmres  5999  elsnres  6008  dfima2  6049  elima3  6054  imadmrn  6057  imai  6061  args  6079  rniun  6136  xpdifid  6157  ssrnres  6167  dmsnn0  6196  dmsnopg  6202  cnvresima  6219  mptpreima  6227  dfco2  6234  coundi  6236  coundir  6237  resco  6239  imaco  6240  rnco  6241  coiun  6245  coi1  6251  coass  6254  xpco  6278  elsnxp  6280  dfpo2  6285  dffun2OLDOLD  6542  dffun5  6547  imadif  6619  funimaexgOLD  6623  brprcneu  6865  brprcneuALT  6866  dffv2  6973  fndmin  7034  fvn0ssdmfun  7063  abrexco  7235  imaiun  7236  isomin  7329  imaeqsexvOLD  7355  dfoprab2  7463  cbvoprab2  7493  zfun  7728  uniex2  7730  uniuni  7754  elxp4  7916  elxp5  7917  fiun  7939  f1iun  7940  f11o  7943  fvresex  7956  opabex3d  7962  opabex3rd  7963  opabex3  7964  abexssex  7967  abexex  7968  oprabrexex2  7975  releldm2  8040  dfopab2  8049  dfoprab3s  8050  fsplit  8114  frxp  8123  suppvalbr  8161  cnvimadfsn  8169  brtpos2  8229  dfwrecsOLD  8310  wfrfunOLD  8331  dfrecs3  8384  dfrecs3OLD  8385  oarec  8572  oeeu  8613  domen  8974  xpsnen  9067  xpcomco  9074  xpassen  9078  dif1enOLD  9174  inf2  9635  zfinf  9651  axinf2  9652  zfinf2  9654  brttrcl2  9726  ttrcltr  9728  ttrclresv  9729  ttrclselem2  9738  rankuni  9875  scott0  9898  cp  9903  ween  10047  aceq1  10129  aceq0  10130  aceq2  10131  dfac5lem1  10135  dfac5lem2  10136  dfac5lem3  10137  kmlem3  10165  kmlem14  10176  kmlem15  10177  kmlem16  10178  cflem  10257  cflemOLD  10258  cf0  10263  cfval2  10272  cfss  10277  cfslb  10278  fin23lem32  10356  axdc2lem  10460  zfac  10472  ac9  10495  ac9s  10505  axpowndlem3  10611  zfcndrep  10626  zfcndun  10627  zfcndpow  10628  zfcndinf  10630  zfcndac  10631  axgroth5  10836  axgroth2  10837  axgroth6  10840  axgroth3  10843  axgroth4  10844  grothprim  10846  grothtsk  10847  genpass  11021  ltexprlem1  11048  ltexprlem4  11051  supaddc  12207  supadd  12208  supmul1  12209  supmullem2  12211  2rexuz  12914  nnwos  12929  hashgt23el  14440  hashfun  14453  wwlktovfo  14975  xpcogend  14991  cbvsum  15709  cbvsumv  15710  cbvprod  15927  cbvprodv  15928  prodeq1i  15930  iprodmul  16017  maxprmfct  16726  4sqlem12  16974  vdwmc  16996  cshwrepswhash1  17120  imasleval  17553  isacs2  17663  cicsym  17815  gsumval3eu  19883  lidlnz  21201  isbasis2g  22884  tgval2  22892  ntreq0  23013  lmff  23237  cmpfi  23344  is1stc2  23378  1stcelcls  23397  unisngl  23463  isfbas2  23771  elfg  23807  alexsubALTlem3  23985  ustfilxp  24149  metrest  24461  metuel2  24502  restmetu  24507  dchrvmasumlema  27461  elold  27825  lrrecfr  27893  sleadd1  27939  addsuniflem  27951  addsasslem1  27953  addsasslem2  27954  mulsuniflem  28092  addsdilem1  28094  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  renegscl  28347  readdscl  28348  remulscl  28351  istrkg2ld  28385  istrkg3ld  28386  1loopgrvd2  29429  wwlksnextsurj  29828  isgrpo  30424  nmo  32417  reuxfrdf  32418  rexunirn  32419  dmrab  32424  disjorf  32506  fcoinvbr  32532  mpomptxf  32601  fpwrelmapffslem  32655  1arithidom  33498  ordtconnlem1  33901  ddemeas  34213  omssubaddlem  34277  omssubadd  34278  eulerpartlemgvv  34354  bnj89  34698  bnj133  34704  bnj1019  34756  bnj1101  34761  bnj1109  34763  bnj1143  34767  bnj1198  34772  bnj1304  34796  bnj605  34884  bnj607  34893  bnj600  34896  bnj865  34900  bnj916  34910  bnj983  34928  bnj985v  34930  bnj985  34931  bnj996  34933  bnj1033  34946  bnj1083  34955  bnj1090  34956  bnj1093  34957  bnj1110  34959  bnj1128  34967  bnj1145  34970  bnj1171  34977  bnj1172  34978  bnj1174  34980  bnj1176  34982  bnj1186  34984  bnj1189  34986  bnj1253  34994  bnj1279  34995  bnj1371  35006  bnj1374  35008  bnj1312  35035  exdifsn  35056  fineqvrep  35072  fineqvpow  35073  lfuhgr3  35088  loop1cycl  35105  satfvsucsuc  35333  satf0op  35345  axextprim  35664  axrepprim  35665  axunprim  35666  axpowprim  35667  axregprim  35668  axinfprim  35669  axacprim  35670  dftr6  35714  coep  35715  coepr  35716  dffr5  35717  cnvco1  35722  cnvco2  35723  eldm3  35724  fundmpss  35730  dfdm5  35736  dfrn5  35737  elima4  35739  axextdfeq  35761  19.12b  35765  axextndbi  35768  brtxp  35844  brpprod  35849  brsset  35853  dfon3  35856  brtxpsd  35858  elfix  35867  dffix2  35869  sscoid  35877  dffun10  35878  elfuns  35879  elsingles  35882  snelsingles  35886  dfiota3  35887  brimg  35901  brapply  35902  brcup  35903  brcap  35904  brsuccf  35905  funpartlem  35906  brrestrict  35913  dfrecs2  35914  dfrdg4  35915  sumeq2si  36166  prodeq2si  36168  cbvoprab2vw  36202  cbvoprab23vw  36204  cbvprodvw2  36211  neifg  36335  bj-equsexval  36624  bj-eeanvw  36677  bj-substw  36686  eliminable-abelv  36833  eliminable-abelab  36834  bj-denoteslem  36835  bj-rexvw  36844  bj-csbsnlem  36867  bj-gabima  36904  bj-snsetex  36927  bj-elsngl  36932  bj-snglc  36933  bj-abex  36994  bj-clex  36995  bj-clel3gALT  37012  bj-nul  37020  bj-dfid2ALT  37029  bj-restpw  37056  bj-restuni  37061  bj-dfmpoa  37082  bj-opabco  37152  bj-xpcossxp  37153  bj-imdirco  37154  mptsnunlem  37302  topdifinffinlem  37311  difunieq  37338  wl-dfclab  37560  poimirlem26  37616  ismblfin  37631  itg2addnclem3  37643  itg2addnc  37644  ismgmOLD  37820  sbcexfi  38087  sbccom2lem  38094  eldmres  38234  ecinn0  38317  ineleq  38318  moantr  38328  rnxrn  38362  rnxrnres  38363  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  38623  prtlem16  38833  prter2  38845  islshpat  38981  islpln5  39500  islvol5  39544  pmapglb  39735  polval2N  39871  cdlemftr3  40530  dibelval3  41112  dicelval3  41145  dihglb2  41307  sn-axrep5v  42213  prjspeclsp  42582  euabsn2w  42649  diophrex  42745  onsupmaxb  43210  nnoeomeqom  43283  tfsconcatlem  43307  tfsconcat0i  43316  rp-isfinite6  43489  snen1g  43495  relintab  43554  imaiun1  43622  coiun1  43623  clsk3nimkb  44011  expandexn  44261  ismnuprim  44266  rr-groth  44271  ismnushort  44273  rr-grothshortbi  44275  19.36vv  44355  19.37vv  44357  pm11.58  44362  pm11.6  44364  pm13.192  44382  2sbc5g  44388  iotasbc2  44392  onfrALTlem5  44515  onfrALTlem1  44521  ax6e2nd  44531  2sb5nd  44533  en3lplem2VD  44816  onfrALTlem5VD  44857  relopabVD  44873  ax6e2ndVD  44880  2sb5ndVD  44882  ax6e2ndALT  44902  2sb5ndALT  44904  dfac5prim  44963  brpermmodel  44976  permaxrep  44979  rfcnnnub  45008  stoweidlem34  46011  stoweidlem35  46012  stoweidlem60  46037  smfpimcc  46785  ichexmpl1  47431  sprid  47436  dfgric2  47876  usgrgrtrirex  47910  grlimgrtri  47956  eliunxp2  48257  mosssn2  48743  coxp  48759  istermc  49308  setrec1lem3  49501  elpglem3  49525  eximp-surprise  49596