Theorem exbii 1867

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

Syntax hints:   ↔ wb 208  ∃wex 1798

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

This theorem depends on definitions:  df-bi 209  df-ex 1799

This theorem is referenced by:  2exbii  1868  3exbii  1869  exanali  1878  exancom  1880  19.43  1901  19.41vv  1969  19.41vvv  1970  19.41vvvv  1971  exdistr  1973  exdistr2  1977  3exdistr  1979  19.12vvv  2013  excom13  2197  exrot4  2199  2sb5  2311  dfsb7  2312  eeor  2364  19.12vv  2377  eean  2378  eeeanv  2380  ee4anv  2381  ee4anvOLD  2382  2sb8ef  2386  equsexALT  2449  2sb5rf  2502  2sb8e  2560  mo4  2592  eu6lem  2599  sb8eulem  2624  cbvmovw  2628  cbvmow  2629  eu1  2636  sbmo  2640  2moswapv  2655  2moswap  2670  euae  2685  issettru  2839  issetlem  2841  clabel  2906  sbabel  2955  nabbib  3059  rextru  3092  rexbii2  3104  r2exlem  3150  r19.41v  3191  r3ex  3200  r19.41  3265  rexcom4  3288  2ex2rexrot  3296  rexv  3480  ceqsex2  3503  ceqsex2v  3504  ceqsex3v  3505  gencbvex  3509  spc3egv  3561  spc3gv  3562  ceqsrexv  3613  rexrab2  3661  euxfrw  3682  euxfr  3684  euind  3685  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  reuind  3714  2reu5lem3  3718  2reu5  3719  2rmoswap  3722  sbcimdv  3810  sbcg  3814  sbccomlemOLD  3821  rmo2  3838  rmoanim  3845  rmoanimALT  3846  rexun  4146  reupick3  4280  euelss  4282  ndisj  4320  inn0f  4321  pssnel  4422  rexsns  4627  exsnrex  4636  snprc  4673  euabsn2  4681  reusn  4683  eusn  4686  elpreqpr  4822  elunirab  4877  uniprg  4878  uniun  4885  uniinOLD  4887  uni0b  4889  uniintsn  4940  iuncom4  4955  dfiun2g  4984  iunn0  5021  iunxiun  5051  disjor  5079  cbvopab2  5173  cbvopab2v  5176  unopab  5177  axrep1  5225  axrep4v  5229  axrep4  5230  axrep4OLD  5231  axrep5  5232  axrep6  5233  axrep6OLD  5234  zfrep6  5236  zfrep4  5240  axsepgfromrep  5241  axnulALT  5251  0ex  5254  vnexOLD  5265  inex1  5270  inuni  5303  axpweq  5304  zfpow  5320  axpow2  5321  vpwex  5331  zfpair  5375  zfpair2  5388  prex  5392  elOLD  5403  eqvinop  5452  copsexgw  5455  copsexgwOLD  5456  copsexg  5457  opabn0  5520  iunopab  5526  dfid2  5540  dfid3  5541  opeliunxp  5710  opeliun2xp  5711  xpiundi  5714  xpiundir  5715  elvvv  5719  csbxp  5744  eliunxp  5805  exopxfr  5811  relop  5818  opelco2g  5835  cnvco  5857  cnvuni  5858  dfdm3  5859  dfrn2  5860  dfrn3  5861  elrng  5863  dfdm4  5867  csbdm  5869  eldm2g  5871  dmun  5882  dmin  5883  dmiun  5885  dmuni  5886  dmopab  5887  dmi  5893  dmep  5895  rnep  5899  dmxp  5901  rnopab  5926  dmcosseq  5950  dmcosseqOLD  5951  dmcosseqOLDOLD  5952  dmres  5994  elsnres  6003  dfima2  6047  elima3  6052  imadmrn  6055  imai  6059  args  6077  rniun  6128  xpdifid  6149  ssrnres  6159  dmsnn0  6189  dmsnopg  6195  cnvresima  6212  mptpreima  6220  dfco2  6227  coundi  6229  coundir  6230  resco  6232  imaco  6233  rnco  6234  rncoOLD  6235  coiun  6239  coi1  6245  coass  6248  xpco  6271  elsnxp  6273  dfpo2  6278  dffun5  6530  imadif  6600  tz6.12-2  6849  brprcneu  6852  brprcneuALT  6853  dffv2  6957  fndmin  7021  fvn0ssdmfun  7050  abrexco  7223  imaiun  7224  isomin  7316  imaeqsexvOLD  7342  dfoprab2  7449  cbvoprab2  7479  zfun  7714  uniex2  7716  uniuni  7740  elxp4  7898  elxp5  7899  fiun  7919  f1iun  7920  f11o  7923  fvresex  7936  opabex3d  7941  opabex3rd  7942  opabex3  7943  abexssex  7946  abexex  7947  oprabrexex2  7954  releldm2  8019  dfopab2  8028  dfoprab3s  8029  fsplit  8090  frxp  8100  suppvalbr  8138  cnvimadfsn  8146  brtpos2  8206  dfrecs3  8337  oarec  8525  oeeu  8567  domen  8936  xpsnen  9027  xpcomco  9033  xpassen  9037  inf2  9572  zfinf  9588  axinf2  9589  zfinf2  9591  brttrcl2  9663  ttrcltr  9665  ttrclresv  9666  ttrclselem2  9675  rankuni  9815  scott0  9838  cp  9843  ween  9985  aceq1  10067  aceq0  10068  aceq2  10069  dfac5lem1  10073  dfac5lem2  10074  dfac5lem3  10075  kmlem3  10103  kmlem14  10114  kmlem15  10115  kmlem16  10116  cflem  10195  cflemOLD  10196  cf0  10201  cfval2  10211  cfss  10216  cfslb  10217  fin23lem32  10295  axdc2lem  10399  zfac  10411  ac9  10434  ac9s  10444  axpowndlem3  10551  zfcndrep  10566  zfcndun  10567  zfcndpow  10568  zfcndinf  10570  zfcndac  10571  axgroth5  10776  axgroth2  10777  axgroth6  10780  axgroth3  10783  axgroth4  10784  grothprim  10786  grothtsk  10787  genpass  10961  ltexprlem1  10988  ltexprlem4  10991  supaddc  12153  supadd  12154  supmul1  12155  supmullem2  12157  2rexuz  12895  nnwos  12910  hashgt23el  14431  hashfun  14444  wwlktovfo  14965  xpcogend  14981  cbvsum  15713  cbvsumv  15714  cbvprod  15934  cbvprodv  15935  prodeq1i  15937  iprodmul  16024  maxprmfct  16735  4sqlem12  16983  vdwmc  17005  cshwrepswhash1  17129  imasleval  17562  isacs2  17676  cicsym  17828  gsumval3eu  19935  lidlnz  21300  isbasis2g  22996  tgval2  23004  ntreq0  23125  lmff  23349  cmpfi  23456  is1stc2  23490  1stcelcls  23509  unisngl  23575  isfbas2  23883  elfg  23919  alexsubALTlem3  24097  ustfilxp  24261  metrest  24572  metuel2  24613  restmetu  24618  dchrvmasumlema  27552  elold  27940  lrrecfr  28024  leadds1  28070  addsuniflem  28082  addsasslem1  28084  addsasslem2  28085  mulsuniflem  28230  addsdilem1  28232  addsdilem2  28233  mulsasslem1  28244  mulsasslem2  28245  elreno2  28576  renegscl  28579  readdscl  28580  remulscl  28583  istrkg2ld  28617  istrkg3ld  28618  1loopgrvd2  29661  wwlksnextsurj  30057  isgrpo  30657  nmo  32648  reuxfrdf  32649  rexunirn  32650  dmrab  32655  disjorf  32739  fcoinvbr  32765  mpomptxf  32841  fpwrelmapffslem  32895  1arithidom  33694  ordtconnlem1  34182  ddemeas  34494  omssubaddlem  34557  omssubadd  34558  eulerpartlemgvv  34634  bnj89  34978  bnj133  34984  bnj1019  35036  bnj1101  35041  bnj1109  35043  bnj1143  35046  bnj1198  35051  bnj1304  35075  bnj605  35163  bnj607  35172  bnj600  35175  bnj865  35179  bnj916  35189  bnj983  35207  bnj985v  35209  bnj985  35210  bnj996  35212  bnj1033  35225  bnj1083  35234  bnj1090  35235  bnj1093  35236  bnj1110  35238  bnj1128  35246  bnj1145  35249  bnj1171  35256  bnj1172  35257  bnj1174  35259  bnj1176  35261  bnj1186  35263  bnj1189  35265  bnj1253  35273  bnj1279  35274  bnj1371  35285  bnj1374  35287  bnj1312  35314  exdifsn  35335  axnulALT2  35338  axprALT2  35366  fineqvrep  35371  fineqvpow  35372  axreg  35384  axregscl  35385  axregs  35396  axpowg  35403  onvfowev  35420  lfuhgr3  35431  loop1cycl  35448  satfvsucsuc  35676  satf0op  35688  axextprim  36012  axrepprim  36013  axunprim  36014  axpowprim  36015  axregprim  36016  axinfprim  36017  axacprim  36018  dftr6  36062  coep  36063  coepr  36064  dffr5  36065  cnvco1  36070  cnvco2  36071  eldm3  36072  fundmpss  36078  dfdm5  36084  dfrn5  36085  elima4  36087  axextdfeq  36106  19.12b  36110  axextndbi  36113  brtxp  36189  brpprod  36194  brsset  36198  dfon3  36201  brtxpsd  36203  elfix  36212  dffix2  36214  sscoid  36222  dffun10  36223  elfuns  36224  elsingles  36227  snelsingles  36231  dfiota3  36232  brimg  36246  brapply  36247  brcup  36248  brcap  36249  lemsuccf  36250  funpartlem  36253  brrestrict  36260  dfrecs2  36261  dfrdg4  36262  sumeq2si  36523  prodeq2si  36525  cbvoprab2vw  36559  cbvoprab23vw  36561  cbvprodvw2  36568  neifg  36692  regsfromregtco  36859  regsfromunir1  36861  mh-prprimbi  36864  mh-unprimbi  36865  mh-infprim1bi  36867  mh-infprim2bi  36868  mh-infprim3bi  36869  bj-df-sb  37083  bj-dfsbc  37085  bj-equsexval  37093  bj-eeanvw  37151  bj-substw  37161  eliminable-abelv  37315  eliminable-abelab  37316  bj-denoteslem  37317  bj-rexvw  37326  bj-csbsnlem  37349  bj-gabima  37386  bj-snsetex  37409  bj-elsngl  37414  bj-snglc  37415  bj-abex  37476  bj-clex  37477  bj-clel3gALT  37494  bj-nul  37502  bj-dfid2ALT  37511  bj-rep  37519  bj-axseprep  37520  bj-restpw  37543  bj-restuni  37548  bj-dfmpoa  37569  bj-opabco  37641  bj-xpcossxp  37642  bj-imdirco  37643  mptsnunlem  37793  topdifinffinlem  37802  difunieq  37829  wl-dfclab  38049  poimirlem26  38106  ismblfin  38121  itg2addnclem3  38133  itg2addnc  38134  ismgmOLD  38310  sbcexfi  38577  sbccom2lem  38584  eldmres  38737  ecinn0  38813  ineleq  38814  moantr  38832  dmcnvep  38848  rnxrn  38881  rnxrnres  38882  dmsucmap  38928  dfcoss2  38963  dfcoss3  38964  cosscnv  38966  coss1cnvres  38967  coss2cnvepres  38968  1cossres  38979  cocossss  38986  rncossdmcoss  39005  eldmcoss2  39009  coss0  39029  cossid  39030  dfssr2  39039  eldmqs1cossres  39204  prtlem16  39454  prter2  39466  islshpat  39602  islpln5  40120  islvol5  40164  pmapglb  40355  polval2N  40491  cdlemftr3  41150  dibelval3  41732  dicelval3  41765  dihglb2  41927  sn-axrep5v  42797  prjspeclsp  43155  euabsn2w  43222  diophrex  43317  onsupmaxb  43777  nnoeomeqom  43850  tfsconcatlem  43874  tfsconcat0i  43883  rp-isfinite6  44055  snen1g  44061  relintab  44120  imaiun1  44188  coiun1  44189  clsk3nimkb  44577  expandexn  44826  ismnuprim  44831  rr-groth  44836  ismnushort  44838  rr-grothshortbi  44840  19.36vv  44920  19.37vv  44922  pm11.58  44927  pm11.6  44929  pm13.192  44947  2sbc5g  44953  iotasbc2  44957  onfrALTlem5  45079  onfrALTlem1  45085  ax6e2nd  45095  2sb5nd  45097  en3lplem2VD  45380  onfrALTlem5VD  45421  relopabVD  45437  ax6e2ndVD  45444  2sb5ndVD  45446  ax6e2ndALT  45466  2sb5ndALT  45468  dfac5prim  45527  brpermmodel  45540  permaxrep  45543  permac8prim  45551  rfcnnnub  45577  stoweidlem34  46569  stoweidlem35  46570  stoweidlem60  46595  smfpimcc  47343  ichexmpl1  48036  sprid  48041  dfgric2  48498  usgrgrtrirex  48533  grlimgrtri  48586  eliunxp2  48917  mosssn2  49399  coxp  49415  istermc  50056  setrec1lem3  50271  elpglem3  50295  eximp-surprise  50366