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 1800	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 205  ∃wex 1782

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

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

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  2165  exrot4  2167  2sb5  2273  dfsb7  2277  eeor  2331  eeorOLD  2332  19.12vv  2346  eean  2347  eeeanv  2349  ee4anv  2350  2sb8ef  2355  equsexALT  2420  2sb5rf  2473  2sb8e  2536  mo4  2567  eu6lem  2574  eubii  2586  sb8eulem  2599  cbvmovw  2603  cbvmow  2604  eu1  2613  sbmo  2617  2moswapv  2632  2moswap  2647  euae  2662  elisset  2821  clabel  2886  sbabel  2942  sbabelOLD  2943  nabbi  3048  rexbii2  3180  r2exlem  3232  rexcom4  3234  2ex2rexrot  3236  r19.41v  3277  r19.41  3278  rexcomOLD  3286  isset  3446  rexv  3458  cgsex4g  3477  cgsex4gOLD  3478  ceqsex2  3483  ceqsex2v  3484  ceqsex3v  3485  gencbvex  3489  spc3egv  3543  spc3gv  3544  ceqsrexv  3586  rexabOLD  3633  rexrab2  3638  euxfrw  3657  euxfr  3659  euind  3660  reu6  3662  reu3  3663  2reuswap  3682  2reuswap2  3683  reuind  3689  2reu5lem3  3693  2reu5  3694  2rmoswap  3697  sbcimdv  3791  sbcg  3796  sbccomlem  3804  rmo2  3821  rmoanim  3828  rmoanimALT  3829  rexun  4125  reupick3  4254  euelss  4256  ndisj  4302  abn0OLD  4316  pssnel  4405  rexsns  4606  exsnrex  4617  snprc  4654  euabsn2  4662  reusn  4664  eusn  4667  elpreqpr  4798  elunirab  4856  uniprg  4857  uniprOLD  4859  uniun  4865  uniin  4866  uni0b  4868  uniintsn  4919  iuncom4  4933  dfiun2g  4961  dfiun2gOLD  4962  iunn0  4997  iunxiun  5027  disjor  5055  cbvopab2  5152  cbvopab2v  5156  unopab  5157  axrep1  5211  axrep4  5215  axrep5  5216  axrep6  5217  zfrep4  5221  axsepgfromrep  5222  axnulALT  5229  0ex  5232  vnex  5239  inex1  5242  inuni  5268  axpweq  5288  zfpow  5290  axpow2  5291  axpow3  5292  vpwex  5301  zfpair  5345  zfpair2  5354  el  5358  eqvinop  5402  copsexgw  5405  copsexg  5406  opabn0  5467  iunopab  5473  iunopabOLD  5474  dfid2  5492  dfid3  5493  opeliunxp  5655  xpiundi  5658  xpiundir  5659  elvvv  5663  csbxp  5687  eliunxp  5749  exopxfr  5755  relop  5762  opelco2g  5779  cnvco  5797  cnvuni  5798  dfdm3  5799  dfrn2  5800  dfrn3  5801  elrng  5803  dfdm4  5807  csbdm  5809  eldm2g  5811  dmun  5822  dmin  5823  dmiun  5825  dmuni  5826  dmopab  5827  dmi  5833  dmep  5835  domepOLD  5836  rnep  5839  rnopab  5866  dmcosseq  5885  dmres  5916  elsnres  5934  dfima2  5974  elima3  5979  imadmrn  5982  imai  5985  args  6003  rniun  6056  xpdifid  6076  ssrnres  6086  dmsnn0  6115  dmsnopg  6121  cnvresima  6138  mptpreima  6146  dfco2  6153  coundi  6155  coundir  6156  resco  6158  imaco  6159  rnco  6160  coiun  6164  coi1  6170  coass  6173  xpco  6196  elsnxp  6198  dfpo2  6203  dffun2OLD  6448  dffun5  6453  imadif  6525  funimaexgOLD  6528  brprcneu  6773  brprcneuALT  6774  dffv2  6872  fndmin  6931  fvn0ssdmfun  6961  abrexco  7126  imaiun  7127  isomin  7217  dfoprab2  7342  cbvoprab2  7372  zfun  7598  uniex2  7600  uniuni  7621  elxp4  7778  elxp5  7779  fiun  7794  f1iun  7795  f11o  7798  fvresex  7811  opabex3d  7817  opabex3rd  7818  opabex3  7819  abexssex  7822  abexex  7823  oprabrexex2  7830  releldm2  7893  dfopab2  7901  dfoprab3s  7902  fsplit  7966  fsplitOLD  7967  frxp  7976  suppvalbr  7990  cnvimadfsn  7997  brtpos2  8057  dfwrecsOLD  8138  wfrfunOLD  8159  dfrecs3  8212  dfrecs3OLD  8213  oarec  8402  oeeu  8443  domen  8760  xpsnen  8851  xpcomco  8858  xpassen  8862  dif1en  8954  inf2  9390  zfinf  9406  axinf2  9407  zfinf2  9409  brttrcl2  9481  ttrcltr  9483  ttrclresv  9484  ttrclselem2  9493  rankuni  9630  scott0  9653  cp  9658  ween  9800  aceq1  9882  aceq0  9883  aceq2  9884  dfac5lem1  9888  dfac5lem2  9889  dfac5lem3  9890  kmlem3  9917  kmlem14  9928  kmlem15  9929  kmlem16  9930  cflem  10011  cf0  10016  cfval2  10025  cfss  10030  cfslb  10031  fin23lem32  10109  axdc2lem  10213  zfac  10225  ac9  10248  ac9s  10258  axpowndlem3  10364  zfcndrep  10379  zfcndun  10380  zfcndpow  10381  zfcndinf  10383  zfcndac  10384  axgroth5  10589  axgroth2  10590  axgroth6  10593  axgroth3  10596  axgroth4  10597  grothprim  10599  grothtsk  10600  genpass  10774  ltexprlem1  10801  ltexprlem4  10804  supaddc  11951  supadd  11952  supmul1  11953  supmullem2  11955  2rexuz  12649  nnwos  12664  hashgt23el  14148  hashfun  14161  wwlktovfo  14682  xpcogend  14694  cbvsum  15416  cbvprod  15634  iprodmul  15722  maxprmfct  16423  4sqlem12  16666  vdwmc  16688  cshwrepswhash1  16813  imasleval  17261  isacs2  17371  cicsym  17525  gsumval3eu  19514  lidlnz  20508  isbasis2g  22107  tgval2  22115  ntreq0  22237  lmff  22461  cmpfi  22568  is1stc2  22602  1stcelcls  22621  unisngl  22687  isfbas2  22995  elfg  23031  alexsubALTlem3  23209  ustfilxp  23373  metrest  23689  metuel2  23730  restmetu  23735  dchrvmasumlema  26657  istrkg2ld  26830  istrkg3ld  26831  1loopgrvd2  27879  wwlksnextsurj  28274  isgrpo  28868  nmo  30847  reuxfrdf  30848  rexunirn  30849  dmrab  30853  disjorf  30927  fcoinvbr  30956  mpomptxf  31025  cnvoprabOLD  31064  fpwrelmapffslem  31076  ordtconnlem1  31883  ddemeas  32213  omssubaddlem  32275  omssubadd  32276  eulerpartlemgvv  32352  bnj89  32709  bnj133  32715  bnj1019  32768  bnj1101  32773  bnj1109  32775  bnj1143  32779  bnj1198  32784  bnj1304  32808  bnj605  32896  bnj607  32905  bnj600  32908  bnj865  32912  bnj916  32922  bnj983  32940  bnj985v  32942  bnj985  32943  bnj996  32945  bnj1033  32958  bnj1083  32967  bnj1090  32968  bnj1093  32969  bnj1110  32971  bnj1128  32979  bnj1145  32982  bnj1171  32989  bnj1172  32990  bnj1174  32992  bnj1176  32994  bnj1186  32996  bnj1189  32998  bnj1253  33006  bnj1279  33007  bnj1371  33018  bnj1374  33020  bnj1312  33047  exdifsn  33062  fineqvrep  33073  fineqvpow  33074  lfuhgr3  33090  loop1cycl  33108  satfvsucsuc  33336  satf0op  33348  axextprim  33651  axrepprim  33652  axunprim  33653  axpowprim  33654  axregprim  33655  axinfprim  33656  axacprim  33657  imaeqsexv  33699  dftr6  33727  coep  33728  coepr  33729  dffr5  33730  cnvco1  33735  cnvco2  33736  eldm3  33737  fundmpss  33749  dfdm5  33756  dfrn5  33757  elima4  33759  axextdfeq  33782  19.12b  33786  axextndbi  33789  elold  34062  lrrecfr  34109  brtxp  34191  brpprod  34196  brsset  34200  dfon3  34203  brtxpsd  34205  elfix  34214  dffix2  34216  sscoid  34224  dffun10  34225  elfuns  34226  elsingles  34229  snelsingles  34233  dfiota3  34234  brimg  34248  brapply  34249  brcup  34250  brcap  34251  brsuccf  34252  funpartlem  34253  brrestrict  34260  dfrecs2  34261  dfrdg4  34262  neifg  34569  bj-equsexval  34850  bj-eeanvw  34904  bj-substw  34913  eliminable-abelv  35062  eliminable-abelab  35063  bj-denoteslem  35064  bj-rexvw  35074  bj-csbsnlem  35097  bj-gabima  35137  bj-snsetex  35162  bj-elsngl  35167  bj-snglc  35168  bj-clel3gALT  35230  bj-nul  35236  bj-dfid2ALT  35245  bj-restpw  35272  bj-restuni  35277  bj-dfmpoa  35298  bj-opabco  35368  bj-xpcossxp  35369  bj-imdirco  35370  mptsnunlem  35518  topdifinffinlem  35527  difunieq  35554  wl-dfclab  35756  poimirlem26  35812  ismblfin  35827  itg2addnclem3  35839  itg2addnc  35840  ismgmOLD  36017  sbcexfi  36284  sbccom2lem  36291  eldmres  36416  ecinn0  36492  ineleq  36493  moantr  36501  rnxrn  36531  rnxrnres  36532  dfcoss2  36546  dfcoss3  36547  1cossres  36559  cocossss  36566  rncossdmcoss  36580  eldmcoss2  36584  coss0  36604  cossid  36605  dfssr2  36624  eldmqs1cossres  36778  prtlem16  36890  prter2  36902  islshpat  37038  islpln5  37556  islvol5  37600  pmapglb  37791  polval2N  37927  cdlemftr3  38586  dibelval3  39168  dicelval3  39201  dihglb2  39363  sn-axrep5v  40192  prjspeclsp  40458  diophrex  40604  rp-isfinite6  41132  snen1g  41138  relintab  41198  imaiun1  41266  coiun1  41267  clsk3nimkb  41657  expandexn  41914  ismnuprim  41919  rr-groth  41924  ismnushort  41926  rr-grothshortbi  41928  19.36vv  42008  19.37vv  42010  pm11.58  42015  pm11.6  42017  pm13.192  42035  2sbc5g  42041  iotasbc2  42045  onfrALTlem5  42169  onfrALTlem1  42175  ax6e2nd  42185  2sb5nd  42187  en3lplem2VD  42471  onfrALTlem5VD  42512  relopabVD  42528  ax6e2ndVD  42535  2sb5ndVD  42537  ax6e2ndALT  42557  2sb5ndALT  42559  rfcnnnub  42586  inn0f  42628  stoweidlem34  43582  stoweidlem35  43583  stoweidlem60  43608  smfpimcc  44352  ichexmpl1  44932  sprid  44937  opeliun2xp  45679  eliunxp2  45680  rextru  46160  mosssn2  46173  setrec1lem3  46406  elpglem3  46429  eximp-surprise  46499