Theorem exbii 1846

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

Syntax hints:   ↔ wb 206  ∃wex 1777

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

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

This theorem is referenced by:  2exbii  1847  3exbii  1848  exanali  1858  exancom  1860  19.43  1881  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1954  exdistr2  1958  3exdistr  1960  19.12vvv  1988  excom13  2165  exrot4  2167  2sb5  2281  dfsb7  2283  eeor  2339  eeorOLD  2340  19.12vv  2353  eean  2354  eeeanv  2356  ee4anv  2357  2sb8ef  2362  equsexALT  2427  2sb5rf  2480  2sb8e  2538  mo4  2569  eu6lem  2576  eubii  2588  sb8eulem  2601  cbvmovw  2605  cbvmow  2606  eu1  2613  sbmo  2617  2moswapv  2632  2moswap  2647  euae  2663  issettru  2822  issetlem  2824  clabel  2891  sbabel  2944  sbabelOLD  2945  nabbib  3051  rextru  3083  rexbii2  3096  r2exlem  3149  r19.41v  3195  r3ex  3204  r19.41  3269  rexcom4  3294  rexcomOLD  3297  2ex2rexrot  3304  rexv  3517  cgsex4gOLD  3539  ceqsex2  3547  ceqsex2v  3548  ceqsex3v  3549  gencbvex  3553  spc3egv  3616  spc3gv  3617  ceqsrexv  3668  rexabOLD  3717  rexrab2  3722  euxfrw  3743  euxfr  3745  euind  3746  reu6  3748  reu3  3749  2reuswap  3768  2reuswap2  3769  reuind  3775  2reu5lem3  3779  2reu5  3780  2rmoswap  3783  sbcimdv  3878  sbcg  3883  sbccomlemOLD  3892  rmo2  3909  rmoanim  3916  rmoanimALT  3917  rexun  4219  reupick3  4349  euelss  4351  ndisj  4393  inn0f  4394  pssnel  4494  rexsns  4693  exsnrex  4704  snprc  4742  euabsn2  4750  reusn  4752  eusn  4755  elpreqpr  4891  elunirab  4946  uniprg  4947  uniun  4954  uniin  4955  uni0b  4957  uniintsn  5009  iuncom4  5023  dfiun2g  5053  dfiun2gOLD  5054  iunn0  5090  iunxiun  5120  disjor  5148  cbvopab2  5243  cbvopab2v  5247  unopab  5248  axrep1  5304  axrep4  5308  axrep5  5309  axrep6  5310  zfrep4  5314  axsepgfromrep  5315  axnulALT  5322  0ex  5325  vnex  5332  inex1  5335  inuni  5368  axpweq  5369  zfpow  5384  axpow2  5385  axpow3  5386  vpwex  5395  zfpair  5439  zfpair2  5448  el  5457  eqvinop  5507  copsexgw  5510  copsexg  5511  opabn0  5572  iunopab  5578  iunopabOLD  5579  dfid2  5595  dfid3  5596  opeliunxp  5767  xpiundi  5770  xpiundir  5771  elvvv  5775  csbxp  5799  eliunxp  5862  exopxfr  5868  relop  5875  opelco2g  5892  cnvco  5910  cnvuni  5911  dfdm3  5912  dfrn2  5913  dfrn3  5914  elrng  5916  dfdm4  5920  csbdm  5922  eldm2g  5924  dmun  5935  dmin  5936  dmiun  5938  dmuni  5939  dmopab  5940  dmi  5946  dmep  5948  rnep  5951  dmxp  5953  rnopab  5979  dmcosseq  5999  dmcosseqOLD  6000  dmres  6041  elsnres  6050  dfima2  6091  elima3  6096  imadmrn  6099  imai  6103  args  6122  rniun  6179  xpdifid  6199  ssrnres  6209  dmsnn0  6238  dmsnopg  6244  cnvresima  6261  mptpreima  6269  dfco2  6276  coundi  6278  coundir  6279  resco  6281  imaco  6282  rnco  6283  coiun  6287  coi1  6293  coass  6296  xpco  6320  elsnxp  6322  dfpo2  6327  dffun2OLDOLD  6585  dffun5  6590  imadif  6662  funimaexgOLD  6665  brprcneu  6910  brprcneuALT  6911  dffv2  7017  fndmin  7078  fvn0ssdmfun  7108  abrexco  7281  imaiun  7282  isomin  7373  imaeqsexvOLD  7399  dfoprab2  7508  cbvoprab2  7538  zfun  7771  uniex2  7773  uniuni  7797  elxp4  7962  elxp5  7963  fiun  7983  f1iun  7984  f11o  7987  fvresex  8000  opabex3d  8006  opabex3rd  8007  opabex3  8008  abexssex  8011  abexex  8012  oprabrexex2  8019  releldm2  8084  dfopab2  8093  dfoprab3s  8094  fsplit  8158  frxp  8167  suppvalbr  8205  cnvimadfsn  8213  brtpos2  8273  dfwrecsOLD  8354  wfrfunOLD  8375  dfrecs3  8428  dfrecs3OLD  8429  oarec  8618  oeeu  8659  domen  9021  xpsnen  9121  xpcomco  9128  xpassen  9132  dif1enOLD  9228  inf2  9692  zfinf  9708  axinf2  9709  zfinf2  9711  brttrcl2  9783  ttrcltr  9785  ttrclresv  9786  ttrclselem2  9795  rankuni  9932  scott0  9955  cp  9960  ween  10104  aceq1  10186  aceq0  10187  aceq2  10188  dfac5lem1  10192  dfac5lem2  10193  dfac5lem3  10194  kmlem3  10222  kmlem14  10233  kmlem15  10234  kmlem16  10235  cflem  10314  cflemOLD  10315  cf0  10320  cfval2  10329  cfss  10334  cfslb  10335  fin23lem32  10413  axdc2lem  10517  zfac  10529  ac9  10552  ac9s  10562  axpowndlem3  10668  zfcndrep  10683  zfcndun  10684  zfcndpow  10685  zfcndinf  10687  zfcndac  10688  axgroth5  10893  axgroth2  10894  axgroth6  10897  axgroth3  10900  axgroth4  10901  grothprim  10903  grothtsk  10904  genpass  11078  ltexprlem1  11105  ltexprlem4  11108  supaddc  12262  supadd  12263  supmul1  12264  supmullem2  12266  2rexuz  12965  nnwos  12980  hashgt23el  14473  hashfun  14486  wwlktovfo  15007  xpcogend  15023  cbvsum  15743  cbvsumv  15744  cbvprod  15961  cbvprodv  15962  prodeq1i  15964  iprodmul  16051  maxprmfct  16756  4sqlem12  17003  vdwmc  17025  cshwrepswhash1  17150  imasleval  17601  isacs2  17711  cicsym  17865  gsumval3eu  19946  lidlnz  21275  isbasis2g  22976  tgval2  22984  ntreq0  23106  lmff  23330  cmpfi  23437  is1stc2  23471  1stcelcls  23490  unisngl  23556  isfbas2  23864  elfg  23900  alexsubALTlem3  24078  ustfilxp  24242  metrest  24558  metuel2  24599  restmetu  24604  dchrvmasumlema  27562  elold  27926  lrrecfr  27994  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  renegscl  28448  readdscl  28449  remulscl  28452  istrkg2ld  28486  istrkg3ld  28487  1loopgrvd2  29539  wwlksnextsurj  29933  isgrpo  30529  nmo  32518  reuxfrdf  32519  rexunirn  32520  dmrab  32525  disjorf  32601  fcoinvbr  32627  mpomptxf  32695  cnvoprabOLD  32734  fpwrelmapffslem  32746  1arithidom  33530  ordtconnlem1  33870  ddemeas  34200  omssubaddlem  34264  omssubadd  34265  eulerpartlemgvv  34341  bnj89  34697  bnj133  34703  bnj1019  34755  bnj1101  34760  bnj1109  34762  bnj1143  34766  bnj1198  34771  bnj1304  34795  bnj605  34883  bnj607  34892  bnj600  34895  bnj865  34899  bnj916  34909  bnj983  34927  bnj985v  34929  bnj985  34930  bnj996  34932  bnj1033  34945  bnj1083  34954  bnj1090  34955  bnj1093  34956  bnj1110  34958  bnj1128  34966  bnj1145  34969  bnj1171  34976  bnj1172  34977  bnj1174  34979  bnj1176  34981  bnj1186  34983  bnj1189  34985  bnj1253  34993  bnj1279  34994  bnj1371  35005  bnj1374  35007  bnj1312  35034  exdifsn  35055  fineqvrep  35071  fineqvpow  35072  lfuhgr3  35087  loop1cycl  35105  satfvsucsuc  35333  satf0op  35345  axextprim  35663  axrepprim  35664  axunprim  35665  axpowprim  35666  axregprim  35667  axinfprim  35668  axacprim  35669  dftr6  35713  coep  35714  coepr  35715  dffr5  35716  cnvco1  35721  cnvco2  35722  eldm3  35723  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  36204  cbvoprab23vw  36206  cbvprodvw2  36213  neifg  36337  bj-equsexval  36626  bj-eeanvw  36679  bj-substw  36688  eliminable-abelv  36835  eliminable-abelab  36836  bj-denoteslem  36837  bj-rexvw  36846  bj-csbsnlem  36869  bj-gabima  36906  bj-snsetex  36929  bj-elsngl  36934  bj-snglc  36935  bj-abex  36996  bj-clex  36997  bj-clel3gALT  37014  bj-nul  37022  bj-dfid2ALT  37031  bj-restpw  37058  bj-restuni  37063  bj-dfmpoa  37084  bj-opabco  37154  bj-xpcossxp  37155  bj-imdirco  37156  mptsnunlem  37304  topdifinffinlem  37313  difunieq  37340  wl-dfclab  37550  poimirlem26  37606  ismblfin  37621  itg2addnclem3  37633  itg2addnc  37634  ismgmOLD  37810  sbcexfi  38077  sbccom2lem  38084  eldmres  38226  ecinn0  38309  ineleq  38310  moantr  38320  rnxrn  38354  rnxrnres  38355  dfcoss2  38369  dfcoss3  38370  cosscnv  38372  coss1cnvres  38373  coss2cnvepres  38374  1cossres  38385  cocossss  38392  rncossdmcoss  38411  eldmcoss2  38415  coss0  38435  cossid  38436  dfssr2  38455  eldmqs1cossres  38615  prtlem16  38825  prter2  38837  islshpat  38973  islpln5  39492  islvol5  39536  pmapglb  39727  polval2N  39863  cdlemftr3  40522  dibelval3  41104  dicelval3  41137  dihglb2  41299  sn-axrep5v  42209  prjspeclsp  42567  euabsn2w  42634  diophrex  42731  onsupmaxb  43200  nnoeomeqom  43274  tfsconcatlem  43298  tfsconcat0i  43307  rp-isfinite6  43480  snen1g  43486  relintab  43545  imaiun1  43613  coiun1  43614  clsk3nimkb  44002  expandexn  44258  ismnuprim  44263  rr-groth  44268  ismnushort  44270  rr-grothshortbi  44272  19.36vv  44352  19.37vv  44354  pm11.58  44359  pm11.6  44361  pm13.192  44379  2sbc5g  44385  iotasbc2  44389  onfrALTlem5  44513  onfrALTlem1  44519  ax6e2nd  44529  2sb5nd  44531  en3lplem2VD  44815  onfrALTlem5VD  44856  relopabVD  44872  ax6e2ndVD  44879  2sb5ndVD  44881  ax6e2ndALT  44901  2sb5ndALT  44903  rfcnnnub  44936  stoweidlem34  45955  stoweidlem35  45956  stoweidlem60  45981  smfpimcc  46729  ichexmpl1  47343  sprid  47348  dfgric2  47768  usgrgrtrirex  47799  grlimgrtri  47820  opeliun2xp  48057  eliunxp2  48058  mosssn2  48548  setrec1lem3  48781  elpglem3  48805  eximp-surprise  48878