Theorem exbii 1851

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

Syntax hints:   ↔ wb 205  ∃wex 1783

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

This theorem depends on definitions:  df-bi 206  df-ex 1784

This theorem is referenced by:  2exbii  1852  3exbii  1853  exanali  1863  exancom  1865  19.43  1886  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistr  1959  exdistr2  1963  3exdistr  1965  19.12vvv  1993  excom13  2166  exrot4  2168  2sb5  2275  dfsb7  2279  eeor  2333  19.12vv  2347  eean  2348  eeeanv  2350  ee4anv  2351  2sb8ev  2354  equsexALT  2419  2sb5rf  2472  2sb8e  2535  mo4  2566  eu6lem  2573  eubii  2585  sb8eulem  2598  cbvmovw  2602  cbvmow  2603  eu1  2612  sbmo  2616  2moswapv  2631  2moswap  2646  euae  2661  elisset  2820  clabel  2884  sbabel  2940  sbabelOLD  2941  nabbi  3046  rexbii2  3175  rexcom4  3179  2ex2rexrot  3180  r2exlem  3230  r19.41v  3273  r19.41  3274  rexcom  3281  isset  3435  rexv  3447  cgsex4g  3466  cgsex4gOLD  3467  ceqsex2  3472  ceqsex2v  3473  ceqsex3v  3474  gencbvex  3478  spc3egv  3532  spc3gv  3533  ceqsrexv  3578  rexabOLD  3625  rexrab2  3632  euxfrw  3651  euxfr  3653  euind  3654  reu6  3656  reu3  3657  2reuswap  3676  2reuswap2  3677  reuind  3683  2reu5lem3  3687  2reu5  3688  2rmoswap  3691  sbcimdv  3786  sbcg  3791  sbccomlem  3799  rmo2  3816  rmoanim  3823  rmoanimALT  3824  rexun  4120  reupick3  4250  euelss  4252  ndisj  4298  abn0OLD  4312  pssnel  4401  rexsns  4602  exsnrex  4613  snprc  4650  euabsn2  4658  reusn  4660  eusn  4663  elpreqpr  4794  elunirab  4852  uniprg  4853  uniprOLD  4855  uniun  4861  uniin  4862  uni0b  4864  uniintsn  4915  iuncom4  4929  dfiun2g  4957  iunn0  4992  iunxiun  5022  disjor  5050  cbvopab2  5147  cbvopab2v  5151  unopab  5152  axrep1  5206  axrep4  5210  axrep5  5211  axrep6  5212  zfrep4  5215  axsepgfromrep  5216  axnulALT  5223  0ex  5226  vnex  5233  inex1  5236  inuni  5262  axpweq  5282  zfpow  5284  axpow2  5285  axpow3  5286  vpwex  5295  zfpair  5339  zfpair2  5348  eqvinop  5395  copsexgw  5398  copsexg  5399  opabn0  5459  iunopab  5465  dfid2  5482  dfid3  5483  opeliunxp  5645  xpiundi  5648  xpiundir  5649  elvvv  5653  csbxp  5676  eliunxp  5735  exopxfr  5741  relop  5748  opelco2g  5765  cnvco  5783  cnvuni  5784  dfdm3  5785  dfrn2  5786  dfrn3  5787  elrng  5789  dfdm4  5793  csbdm  5795  eldm2g  5797  dmun  5808  dmin  5809  dmiun  5811  dmuni  5812  dmopab  5813  dmi  5819  dmep  5821  domepOLD  5822  rnep  5825  rnopab  5852  dmcosseq  5871  dmres  5902  elsnres  5920  dfima2  5960  elima3  5965  imadmrn  5968  imai  5971  args  5989  rniun  6040  xpdifid  6060  ssrnres  6070  dmsnn0  6099  dmsnopg  6105  cnvresima  6122  mptpreima  6130  dfco2  6138  coundi  6140  coundir  6141  resco  6143  imaco  6144  rnco  6145  coiun  6149  coi1  6155  coass  6158  xpco  6181  elsnxp  6183  dfpo2  6188  dffun2  6428  dffun5  6431  imadif  6502  funimaexg  6504  brprcneu  6747  fvprc  6748  dffv2  6845  fndmin  6904  fvn0ssdmfun  6934  abrexco  7099  imaiun  7100  isomin  7188  dfoprab2  7311  cbvoprab2  7341  zfun  7567  uniex2  7569  uniuni  7590  elxp4  7743  elxp5  7744  fiun  7759  f1iun  7760  f11o  7763  fvresex  7776  opabex3d  7781  opabex3rd  7782  opabex3  7783  abexssex  7786  abexex  7787  oprabrexex2  7794  releldm2  7857  dfopab2  7865  dfoprab3s  7866  fsplit  7928  fsplitOLD  7929  frxp  7938  suppvalbr  7952  cnvimadfsn  7959  brtpos2  8019  dfwrecsOLD  8100  wfrfunOLD  8121  dfrecs3  8174  dfrecs3OLD  8175  oarec  8355  oeeu  8396  domen  8706  xpsnen  8796  xpcomco  8802  xpassen  8806  dif1en  8907  inf2  9311  zfinf  9327  axinf2  9328  zfinf2  9330  rankuni  9552  scott0  9575  cp  9580  ween  9722  aceq1  9804  aceq0  9805  aceq2  9806  dfac5lem1  9810  dfac5lem2  9811  dfac5lem3  9812  kmlem3  9839  kmlem14  9850  kmlem15  9851  kmlem16  9852  cflem  9933  cf0  9938  cfval2  9947  cfss  9952  cfslb  9953  fin23lem32  10031  axdc2lem  10135  zfac  10147  ac9  10170  ac9s  10180  axpowndlem3  10286  zfcndrep  10301  zfcndun  10302  zfcndpow  10303  zfcndinf  10305  zfcndac  10306  axgroth5  10511  axgroth2  10512  axgroth6  10515  axgroth3  10518  axgroth4  10519  grothprim  10521  grothtsk  10522  genpass  10696  ltexprlem1  10723  ltexprlem4  10726  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  2rexuz  12569  nnwos  12584  hashgt23el  14067  hashfun  14080  wwlktovfo  14601  xpcogend  14613  cbvsum  15335  cbvprod  15553  iprodmul  15641  maxprmfct  16342  4sqlem12  16585  vdwmc  16607  cshwrepswhash1  16732  imasleval  17169  isacs2  17279  cicsym  17433  gsumval3eu  19420  lidlnz  20412  isbasis2g  22006  tgval2  22014  ntreq0  22136  lmff  22360  cmpfi  22467  is1stc2  22501  1stcelcls  22520  unisngl  22586  isfbas2  22894  elfg  22930  alexsubALTlem3  23108  ustfilxp  23272  metrest  23586  metuel2  23627  restmetu  23632  dchrvmasumlema  26553  istrkg2ld  26725  istrkg3ld  26726  1loopgrvd2  27773  wwlksnextsurj  28166  isgrpo  28760  nmo  30739  reuxfrdf  30740  rexunirn  30741  dmrab  30745  disjorf  30819  fcoinvbr  30848  mpomptxf  30918  cnvoprabOLD  30957  fpwrelmapffslem  30969  ordtconnlem1  31776  ddemeas  32104  omssubaddlem  32166  omssubadd  32167  eulerpartlemgvv  32243  bnj89  32600  bnj133  32606  bnj1019  32659  bnj1101  32664  bnj1109  32666  bnj1143  32670  bnj1198  32675  bnj1304  32699  bnj605  32787  bnj607  32796  bnj600  32799  bnj865  32803  bnj916  32813  bnj983  32831  bnj985v  32833  bnj985  32834  bnj996  32836  bnj1033  32849  bnj1083  32858  bnj1090  32859  bnj1093  32860  bnj1110  32862  bnj1128  32870  bnj1145  32873  bnj1171  32880  bnj1172  32881  bnj1174  32883  bnj1176  32885  bnj1186  32887  bnj1189  32889  bnj1253  32897  bnj1279  32898  bnj1371  32909  bnj1374  32911  bnj1312  32938  exdifsn  32953  fineqvrep  32964  fineqvpow  32965  lfuhgr3  32981  loop1cycl  32999  satfvsucsuc  33227  satf0op  33239  axextprim  33542  axrepprim  33543  axunprim  33544  axpowprim  33545  axregprim  33546  axinfprim  33547  axacprim  33548  imaeqsexv  33593  dftr6  33624  coep  33625  coepr  33626  dffr5  33627  cnvco1  33632  cnvco2  33633  eldm3  33634  fundmpss  33646  dfdm5  33653  dfrn5  33654  elima4  33656  axextdfeq  33679  19.12b  33683  axextndbi  33686  brttrcl2  33700  ttrcltr  33702  ttrclresv  33703  ttrclselem2  33712  elold  33980  lrrecfr  34027  brtxp  34109  brpprod  34114  brsset  34118  dfon3  34121  brtxpsd  34123  elfix  34132  dffix2  34134  sscoid  34142  dffun10  34143  elfuns  34144  elsingles  34147  snelsingles  34151  dfiota3  34152  brimg  34166  brapply  34167  brcup  34168  brcap  34169  brsuccf  34170  funpartlem  34171  brrestrict  34178  dfrecs2  34179  dfrdg4  34180  neifg  34487  bj-equsexval  34768  bj-eeanvw  34822  bj-substw  34831  eliminable-abelv  34980  eliminable-abelab  34981  bj-denoteslem  34982  bj-rexvw  34992  bj-csbsnlem  35015  bj-gabima  35055  bj-snsetex  35080  bj-elsngl  35085  bj-snglc  35086  bj-clel3gALT  35148  bj-nul  35154  bj-dfid2ALT  35163  bj-restpw  35190  bj-restuni  35195  bj-dfmpoa  35216  bj-opabco  35286  bj-xpcossxp  35287  bj-imdirco  35288  mptsnunlem  35436  topdifinffinlem  35445  difunieq  35472  wl-dfclab  35674  poimirlem26  35730  ismblfin  35745  itg2addnclem3  35757  itg2addnc  35758  ismgmOLD  35935  sbcexfi  36202  sbccom2lem  36209  eldmres  36335  ecinn0  36412  ineleq  36413  moantr  36421  rnxrn  36451  rnxrnres  36452  dfcoss2  36466  dfcoss3  36467  1cossres  36479  cocossss  36486  rncossdmcoss  36500  eldmcoss2  36504  coss0  36524  cossid  36525  dfssr2  36544  eldmqs1cossres  36698  prtlem16  36810  prter2  36822  islshpat  36958  islpln5  37476  islvol5  37520  pmapglb  37711  polval2N  37847  cdlemftr3  38506  dibelval3  39088  dicelval3  39121  dihglb2  39283  sn-axrep5v  40113  prjspeclsp  40372  diophrex  40513  rp-isfinite6  41023  snen1g  41029  relintab  41080  imaiun1  41148  coiun1  41149  clsk3nimkb  41539  expandexn  41796  ismnuprim  41801  rr-groth  41806  ismnushort  41808  rr-grothshortbi  41810  19.36vv  41890  19.37vv  41892  pm11.58  41897  pm11.6  41899  pm13.192  41917  2sbc5g  41923  iotasbc2  41927  onfrALTlem5  42051  onfrALTlem1  42057  ax6e2nd  42067  2sb5nd  42069  en3lplem2VD  42353  onfrALTlem5VD  42394  relopabVD  42410  ax6e2ndVD  42417  2sb5ndVD  42419  ax6e2ndALT  42439  2sb5ndALT  42441  rfcnnnub  42468  inn0f  42510  stoweidlem34  43465  stoweidlem35  43466  stoweidlem60  43491  smfpimcc  44228  ichexmpl1  44809  sprid  44814  opeliun2xp  45556  eliunxp2  45557  rextru  46037  mosssn2  46050  setrec1lem3  46281  elpglem3  46304  eximp-surprise  46374