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  2338  19.12vv  2351  eean  2352  eeeanv  2354  ee4anv  2355  ee4anvOLD  2356  2sb8ef  2360  equsexALT  2423  2sb5rf  2476  2sb8e  2534  mo4  2566  eu6lem  2573  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  eu1  2610  sbmo  2614  2moswapv  2629  2moswap  2644  euae  2660  issettru  2814  issetlem  2816  clabel  2881  sbabel  2931  nabbib  3035  rextru  3068  rexbii2  3080  r2exlem  3126  r19.41v  3167  r3ex  3176  r19.41  3241  rexcom4  3264  2ex2rexrot  3272  rexv  3457  ceqsex2  3481  ceqsex2v  3482  ceqsex3v  3483  gencbvex  3487  spc3egv  3545  spc3gv  3546  ceqsrexv  3597  rexrab2  3646  euxfrw  3667  euxfr  3669  euind  3670  reu6  3672  reu3  3673  2reuswap  3692  2reuswap2  3693  reuind  3699  2reu5lem3  3703  2reu5  3704  2rmoswap  3707  sbcimdv  3797  sbcg  3801  sbccomlemOLD  3808  rmo2  3825  rmoanim  3832  rmoanimALT  3833  rexun  4136  reupick3  4270  euelss  4272  ndisj  4310  inn0f  4311  pssnel  4411  rexsns  4615  exsnrex  4624  snprc  4661  euabsn2  4669  reusn  4671  eusn  4674  elpreqpr  4810  elunirab  4865  uniprg  4866  uniun  4873  uniin  4874  uni0b  4876  uniintsn  4927  iuncom4  4942  dfiun2g  4972  iunn0  5009  iunxiun  5039  disjor  5067  cbvopab2  5161  cbvopab2v  5164  unopab  5165  axrep1  5213  axrep4v  5217  axrep4  5218  axrep4OLD  5219  axrep5  5220  axrep6  5221  axrep6OLD  5222  zfrep6  5224  zfrep4  5228  axsepgfromrep  5229  axnulALT  5239  0ex  5242  vnexOLD  5253  inex1  5258  inuni  5291  axpweq  5292  zfpow  5308  axpow2  5309  vpwex  5319  zfpair  5363  zfpair2  5376  prex  5380  elOLD  5391  eqvinop  5440  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  opabn0  5508  iunopab  5514  dfid2  5528  dfid3  5529  opeliunxp  5698  opeliun2xp  5699  xpiundi  5702  xpiundir  5703  elvvv  5707  csbxp  5732  eliunxp  5792  exopxfr  5798  relop  5805  opelco2g  5822  cnvco  5840  cnvuni  5841  dfdm3  5842  dfrn2  5843  dfrn3  5844  elrng  5846  dfdm4  5850  csbdm  5852  eldm2g  5854  dmun  5865  dmin  5866  dmiun  5868  dmuni  5869  dmopab  5870  dmi  5876  dmep  5878  rnep  5882  dmxp  5884  rnopab  5909  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  dmres  5977  elsnres  5986  dfima2  6027  elima3  6032  imadmrn  6035  imai  6039  args  6057  rniun  6111  xpdifid  6132  ssrnres  6142  dmsnn0  6171  dmsnopg  6177  cnvresima  6194  mptpreima  6202  dfco2  6209  coundi  6211  coundir  6212  resco  6214  imaco  6215  rnco  6216  rncoOLD  6217  coiun  6221  coi1  6227  coass  6230  xpco  6253  elsnxp  6255  dfpo2  6260  dffun5  6512  imadif  6582  tz6.12-2  6827  brprcneu  6830  brprcneuALT  6831  dffv2  6935  fndmin  6997  fvn0ssdmfun  7026  abrexco  7199  imaiun  7200  isomin  7292  imaeqsexvOLD  7318  dfoprab2  7425  cbvoprab2  7455  zfun  7690  uniex2  7692  uniuni  7716  elxp4  7873  elxp5  7874  fiun  7896  f1iun  7897  f11o  7900  fvresex  7913  opabex3d  7918  opabex3rd  7919  opabex3  7920  abexssex  7923  abexex  7924  oprabrexex2  7931  releldm2  7996  dfopab2  8005  dfoprab3s  8006  fsplit  8067  frxp  8076  suppvalbr  8114  cnvimadfsn  8122  brtpos2  8182  dfrecs3  8312  oarec  8497  oeeu  8539  domen  8908  xpsnen  8999  xpcomco  9005  xpassen  9009  inf2  9544  zfinf  9560  axinf2  9561  zfinf2  9563  brttrcl2  9635  ttrcltr  9637  ttrclresv  9638  ttrclselem2  9647  rankuni  9787  scott0  9810  cp  9815  ween  9957  aceq1  10039  aceq0  10040  aceq2  10041  dfac5lem1  10045  dfac5lem2  10046  dfac5lem3  10047  kmlem3  10075  kmlem14  10086  kmlem15  10087  kmlem16  10088  cflem  10167  cflemOLD  10168  cf0  10173  cfval2  10182  cfss  10187  cfslb  10188  fin23lem32  10266  axdc2lem  10370  zfac  10382  ac9  10405  ac9s  10415  axpowndlem3  10522  zfcndrep  10537  zfcndun  10538  zfcndpow  10539  zfcndinf  10541  zfcndac  10542  axgroth5  10747  axgroth2  10748  axgroth6  10751  axgroth3  10754  axgroth4  10755  grothprim  10757  grothtsk  10758  genpass  10932  ltexprlem1  10959  ltexprlem4  10962  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  2rexuz  12850  nnwos  12865  hashgt23el  14386  hashfun  14399  wwlktovfo  14920  xpcogend  14936  cbvsum  15657  cbvsumv  15658  cbvprod  15878  cbvprodv  15879  prodeq1i  15881  iprodmul  15968  maxprmfct  16679  4sqlem12  16927  vdwmc  16949  cshwrepswhash1  17073  imasleval  17505  isacs2  17619  cicsym  17771  gsumval3eu  19879  lidlnz  21240  isbasis2g  22913  tgval2  22921  ntreq0  23042  lmff  23266  cmpfi  23373  is1stc2  23407  1stcelcls  23426  unisngl  23492  isfbas2  23800  elfg  23836  alexsubALTlem3  24014  ustfilxp  24178  metrest  24489  metuel2  24530  restmetu  24535  dchrvmasumlema  27463  elold  27851  lrrecfr  27935  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  mulsuniflem  28141  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  elreno2  28487  renegscl  28490  readdscl  28491  remulscl  28494  istrkg2ld  28528  istrkg3ld  28529  1loopgrvd2  29572  wwlksnextsurj  29968  isgrpo  30568  nmo  32559  reuxfrdf  32560  rexunirn  32561  dmrab  32566  disjorf  32649  fcoinvbr  32675  mpomptxf  32751  fpwrelmapffslem  32805  1arithidom  33597  ordtconnlem1  34068  ddemeas  34380  omssubaddlem  34443  omssubadd  34444  eulerpartlemgvv  34520  bnj89  34864  bnj133  34870  bnj1019  34922  bnj1101  34927  bnj1109  34929  bnj1143  34932  bnj1198  34937  bnj1304  34961  bnj605  35049  bnj607  35058  bnj600  35061  bnj865  35065  bnj916  35075  bnj983  35093  bnj985v  35095  bnj985  35096  bnj996  35098  bnj1033  35111  bnj1083  35120  bnj1090  35121  bnj1093  35122  bnj1110  35124  bnj1128  35132  bnj1145  35135  bnj1171  35142  bnj1172  35143  bnj1174  35145  bnj1176  35147  bnj1186  35149  bnj1189  35151  bnj1253  35159  bnj1279  35160  bnj1371  35171  bnj1374  35173  bnj1312  35200  exdifsn  35221  axnulALT2  35224  axprALT2  35253  fineqvrep  35258  fineqvpow  35259  axreg  35271  axregscl  35272  axregs  35283  lfuhgr3  35302  loop1cycl  35319  satfvsucsuc  35547  satf0op  35559  axextprim  35883  axrepprim  35884  axunprim  35885  axpowprim  35886  axregprim  35887  axinfprim  35888  axacprim  35889  dftr6  35933  coep  35934  coepr  35935  dffr5  35936  cnvco1  35941  cnvco2  35942  eldm3  35943  fundmpss  35949  dfdm5  35955  dfrn5  35956  elima4  35958  axextdfeq  35977  19.12b  35981  axextndbi  35984  brtxp  36060  brpprod  36065  brsset  36069  dfon3  36072  brtxpsd  36074  elfix  36083  dffix2  36085  sscoid  36093  dffun10  36094  elfuns  36095  elsingles  36098  snelsingles  36102  dfiota3  36103  brimg  36117  brapply  36118  brcup  36119  brcap  36120  lemsuccf  36121  funpartlem  36124  brrestrict  36131  dfrecs2  36132  dfrdg4  36133  sumeq2si  36384  prodeq2si  36386  cbvoprab2vw  36420  cbvoprab23vw  36422  cbvprodvw2  36429  neifg  36553  regsfromregtco  36720  regsfromunir1  36722  mh-prprimbi  36725  mh-unprimbi  36726  mh-infprim1bi  36728  mh-infprim2bi  36729  mh-infprim3bi  36730  bj-df-sb  36944  bj-dfsbc  36946  bj-equsexval  36954  bj-eeanvw  37012  bj-substw  37022  eliminable-abelv  37176  eliminable-abelab  37177  bj-denoteslem  37178  bj-rexvw  37187  bj-csbsnlem  37210  bj-gabima  37247  bj-snsetex  37270  bj-elsngl  37275  bj-snglc  37276  bj-abex  37337  bj-clex  37338  bj-clel3gALT  37355  bj-nul  37363  bj-dfid2ALT  37372  bj-rep  37380  bj-axseprep  37381  bj-restpw  37404  bj-restuni  37409  bj-dfmpoa  37430  bj-opabco  37502  bj-xpcossxp  37503  bj-imdirco  37504  mptsnunlem  37654  topdifinffinlem  37663  difunieq  37690  wl-dfclab  37910  poimirlem26  37967  ismblfin  37982  itg2addnclem3  37994  itg2addnc  37995  ismgmOLD  38171  sbcexfi  38438  sbccom2lem  38445  eldmres  38598  ecinn0  38674  ineleq  38675  moantr  38693  dmcnvep  38709  rnxrn  38742  rnxrnres  38743  dmsucmap  38789  dfcoss2  38824  dfcoss3  38825  cosscnv  38827  coss1cnvres  38828  coss2cnvepres  38829  1cossres  38840  cocossss  38847  rncossdmcoss  38866  eldmcoss2  38870  coss0  38890  cossid  38891  dfssr2  38900  eldmqs1cossres  39065  prtlem16  39315  prter2  39327  islshpat  39463  islpln5  39981  islvol5  40025  pmapglb  40216  polval2N  40352  cdlemftr3  41011  dibelval3  41593  dicelval3  41626  dihglb2  41788  sn-axrep5v  42658  prjspeclsp  43045  euabsn2w  43112  diophrex  43207  onsupmaxb  43667  nnoeomeqom  43740  tfsconcatlem  43764  tfsconcat0i  43773  rp-isfinite6  43945  snen1g  43951  relintab  44010  imaiun1  44078  coiun1  44079  clsk3nimkb  44467  expandexn  44716  ismnuprim  44721  rr-groth  44726  ismnushort  44728  rr-grothshortbi  44730  19.36vv  44810  19.37vv  44812  pm11.58  44817  pm11.6  44819  pm13.192  44837  2sbc5g  44843  iotasbc2  44847  onfrALTlem5  44969  onfrALTlem1  44975  ax6e2nd  44985  2sb5nd  44987  en3lplem2VD  45270  onfrALTlem5VD  45311  relopabVD  45327  ax6e2ndVD  45334  2sb5ndVD  45336  ax6e2ndALT  45356  2sb5ndALT  45358  dfac5prim  45417  brpermmodel  45430  permaxrep  45433  permac8prim  45441  rfcnnnub  45467  stoweidlem34  46462  stoweidlem35  46463  stoweidlem60  46488  smfpimcc  47236  ichexmpl1  47929  sprid  47934  dfgric2  48391  usgrgrtrirex  48426  grlimgrtri  48479  eliunxp2  48810  mosssn2  49292  coxp  49308  istermc  49949  setrec1lem3  50164  elpglem3  50188  eximp-surprise  50259