Theorem exbii 1849

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

Syntax hints:   ↔ wb 206  ∃wex 1780

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

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

This theorem is referenced by:  2exbii  1850  3exbii  1851  exanali  1860  exancom  1862  19.43  1883  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistr  1955  exdistr2  1959  3exdistr  1961  19.12vvv  1995  excom13  2169  exrot4  2171  2sb5  2284  dfsb7  2285  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  3067  rexbii2  3079  r2exlem  3125  r19.41v  3166  r3ex  3175  r19.41  3240  rexcom4  3263  2ex2rexrot  3271  rexv  3468  cgsex4gOLD  3488  ceqsex2  3493  ceqsex2v  3494  ceqsex3v  3495  gencbvex  3499  spc3egv  3557  spc3gv  3558  ceqsrexv  3609  rexrab2  3658  euxfrw  3679  euxfr  3681  euind  3682  reu6  3684  reu3  3685  2reuswap  3704  2reuswap2  3705  reuind  3711  2reu5lem3  3715  2reu5  3716  2rmoswap  3719  sbcimdv  3809  sbcg  3813  sbccomlemOLD  3820  rmo2  3837  rmoanim  3844  rmoanimALT  3845  rexun  4148  reupick3  4282  euelss  4284  ndisj  4322  inn0f  4323  pssnel  4423  rexsns  4628  exsnrex  4637  snprc  4674  euabsn2  4682  reusn  4684  eusn  4687  elpreqpr  4823  elunirab  4878  uniprg  4879  uniun  4886  uniin  4887  uni0b  4889  uniintsn  4940  iuncom4  4955  dfiun2g  4985  iunn0  5022  iunxiun  5052  disjor  5080  cbvopab2  5174  cbvopab2v  5177  unopab  5178  axrep1  5225  axrep4v  5229  axrep4  5230  axrep4OLD  5231  axrep5  5232  axrep6  5233  axrep6OLD  5234  zfrep4  5238  axsepgfromrep  5239  axnulALT  5249  0ex  5252  vnex  5259  inex1  5262  inuni  5295  axpweq  5296  zfpow  5311  axpow2  5312  vpwex  5322  zfpair  5366  zfpair2  5378  el  5387  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  6990  fvn0ssdmfun  7019  abrexco  7190  imaiun  7191  isomin  7283  imaeqsexvOLD  7309  dfoprab2  7416  cbvoprab2  7446  zfun  7681  uniex2  7683  uniuni  7707  elxp4  7864  elxp5  7865  fiun  7887  f1iun  7888  f11o  7891  fvresex  7904  opabex3d  7909  opabex3rd  7910  opabex3  7911  abexssex  7914  abexex  7915  oprabrexex2  7922  releldm2  7987  dfopab2  7996  dfoprab3s  7997  fsplit  8059  frxp  8068  suppvalbr  8106  cnvimadfsn  8114  brtpos2  8174  dfrecs3  8304  oarec  8489  oeeu  8531  domen  8898  xpsnen  8989  xpcomco  8995  xpassen  8999  inf2  9532  zfinf  9548  axinf2  9549  zfinf2  9551  brttrcl2  9623  ttrcltr  9625  ttrclresv  9626  ttrclselem2  9635  rankuni  9775  scott0  9798  cp  9803  ween  9945  aceq1  10027  aceq0  10028  aceq2  10029  dfac5lem1  10033  dfac5lem2  10034  dfac5lem3  10035  kmlem3  10063  kmlem14  10074  kmlem15  10075  kmlem16  10076  cflem  10155  cflemOLD  10156  cf0  10161  cfval2  10170  cfss  10175  cfslb  10176  fin23lem32  10254  axdc2lem  10358  zfac  10370  ac9  10393  ac9s  10403  axpowndlem3  10510  zfcndrep  10525  zfcndun  10526  zfcndpow  10527  zfcndinf  10529  zfcndac  10530  axgroth5  10735  axgroth2  10736  axgroth6  10739  axgroth3  10742  axgroth4  10743  grothprim  10745  grothtsk  10746  genpass  10920  ltexprlem1  10947  ltexprlem4  10950  supaddc  12109  supadd  12110  supmul1  12111  supmullem2  12113  2rexuz  12813  nnwos  12828  hashgt23el  14347  hashfun  14360  wwlktovfo  14881  xpcogend  14897  cbvsum  15618  cbvsumv  15619  cbvprod  15836  cbvprodv  15837  prodeq1i  15839  iprodmul  15926  maxprmfct  16636  4sqlem12  16884  vdwmc  16906  cshwrepswhash1  17030  imasleval  17462  isacs2  17576  cicsym  17728  gsumval3eu  19833  lidlnz  21197  isbasis2g  22892  tgval2  22900  ntreq0  23021  lmff  23245  cmpfi  23352  is1stc2  23386  1stcelcls  23405  unisngl  23471  isfbas2  23779  elfg  23815  alexsubALTlem3  23993  ustfilxp  24157  metrest  24468  metuel2  24509  restmetu  24514  dchrvmasumlema  27467  elold  27855  lrrecfr  27939  leadds1  27985  addsuniflem  27997  addsasslem1  27999  addsasslem2  28000  mulsuniflem  28145  addsdilem1  28147  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  elreno2  28491  renegscl  28494  readdscl  28495  remulscl  28498  istrkg2ld  28532  istrkg3ld  28533  1loopgrvd2  29577  wwlksnextsurj  29973  isgrpo  30572  nmo  32564  reuxfrdf  32565  rexunirn  32566  dmrab  32571  disjorf  32654  fcoinvbr  32680  mpomptxf  32757  fpwrelmapffslem  32811  1arithidom  33618  ordtconnlem1  34081  ddemeas  34393  omssubaddlem  34456  omssubadd  34457  eulerpartlemgvv  34533  bnj89  34877  bnj133  34883  bnj1019  34935  bnj1101  34940  bnj1109  34942  bnj1143  34946  bnj1198  34951  bnj1304  34975  bnj605  35063  bnj607  35072  bnj600  35075  bnj865  35079  bnj916  35089  bnj983  35107  bnj985v  35109  bnj985  35110  bnj996  35112  bnj1033  35125  bnj1083  35134  bnj1090  35135  bnj1093  35136  bnj1110  35138  bnj1128  35146  bnj1145  35149  bnj1171  35156  bnj1172  35157  bnj1174  35159  bnj1176  35161  bnj1186  35163  bnj1189  35165  bnj1253  35173  bnj1279  35174  bnj1371  35185  bnj1374  35187  bnj1312  35214  exdifsn  35235  fineqvrep  35270  fineqvpow  35271  axreg  35283  axregscl  35284  axregs  35295  lfuhgr3  35314  loop1cycl  35331  satfvsucsuc  35559  satf0op  35571  axextprim  35895  axrepprim  35896  axunprim  35897  axpowprim  35898  axregprim  35899  axinfprim  35900  axacprim  35901  dftr6  35945  coep  35946  coepr  35947  dffr5  35948  cnvco1  35953  cnvco2  35954  eldm3  35955  fundmpss  35961  dfdm5  35967  dfrn5  35968  elima4  35970  axextdfeq  35989  19.12b  35993  axextndbi  35996  brtxp  36072  brpprod  36077  brsset  36081  dfon3  36084  brtxpsd  36086  elfix  36095  dffix2  36097  sscoid  36105  dffun10  36106  elfuns  36107  elsingles  36110  snelsingles  36114  dfiota3  36115  brimg  36129  brapply  36130  brcup  36131  brcap  36132  lemsuccf  36133  funpartlem  36136  brrestrict  36143  dfrecs2  36144  dfrdg4  36145  sumeq2si  36396  prodeq2si  36398  cbvoprab2vw  36432  cbvoprab23vw  36434  cbvprodvw2  36441  neifg  36565  regsfromregtr  36668  regsfromunir1  36670  bj-df-sb  36853  bj-equsexval  36861  bj-eeanvw  36914  bj-substw  36923  eliminable-abelv  37070  eliminable-abelab  37071  bj-denoteslem  37072  bj-rexvw  37081  bj-csbsnlem  37104  bj-gabima  37141  bj-snsetex  37164  bj-elsngl  37169  bj-snglc  37170  bj-abex  37231  bj-clex  37232  bj-clel3gALT  37249  bj-nul  37257  bj-dfid2ALT  37266  bj-restpw  37297  bj-restuni  37302  bj-dfmpoa  37323  bj-opabco  37393  bj-xpcossxp  37394  bj-imdirco  37395  mptsnunlem  37543  topdifinffinlem  37552  difunieq  37579  wl-dfclab  37790  poimirlem26  37847  ismblfin  37862  itg2addnclem3  37874  itg2addnc  37875  ismgmOLD  38051  sbcexfi  38318  sbccom2lem  38325  eldmres  38470  ecinn0  38546  ineleq  38547  moantr  38557  dmcnvep  38573  rnxrn  38606  rnxrnres  38607  dmsucmap  38642  dfcoss2  38676  dfcoss3  38677  cosscnv  38679  coss1cnvres  38680  coss2cnvepres  38681  1cossres  38692  cocossss  38699  rncossdmcoss  38718  eldmcoss2  38722  coss0  38742  cossid  38743  dfssr2  38752  eldmqs1cossres  38918  prtlem16  39129  prter2  39141  islshpat  39277  islpln5  39795  islvol5  39839  pmapglb  40030  polval2N  40166  cdlemftr3  40825  dibelval3  41407  dicelval3  41440  dihglb2  41602  sn-axrep5v  42473  prjspeclsp  42855  euabsn2w  42922  diophrex  43017  onsupmaxb  43481  nnoeomeqom  43554  tfsconcatlem  43578  tfsconcat0i  43587  rp-isfinite6  43759  snen1g  43765  relintab  43824  imaiun1  43892  coiun1  43893  clsk3nimkb  44281  expandexn  44530  ismnuprim  44535  rr-groth  44540  ismnushort  44542  rr-grothshortbi  44544  19.36vv  44624  19.37vv  44626  pm11.58  44631  pm11.6  44633  pm13.192  44651  2sbc5g  44657  iotasbc2  44661  onfrALTlem5  44783  onfrALTlem1  44789  ax6e2nd  44799  2sb5nd  44801  en3lplem2VD  45084  onfrALTlem5VD  45125  relopabVD  45141  ax6e2ndVD  45148  2sb5ndVD  45150  ax6e2ndALT  45170  2sb5ndALT  45172  dfac5prim  45231  brpermmodel  45244  permaxrep  45247  permac8prim  45255  rfcnnnub  45281  stoweidlem34  46278  stoweidlem35  46279  stoweidlem60  46304  smfpimcc  47052  ichexmpl1  47715  sprid  47720  dfgric2  48161  usgrgrtrirex  48196  grlimgrtri  48249  eliunxp2  48580  mosssn2  49062  coxp  49078  istermc  49719  setrec1lem3  49934  elpglem3  49958  eximp-surprise  50029