Theorem exbii 1848

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

Syntax hints:   ↔ wb 206  ∃wex 1779

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

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

This theorem is referenced by:  2exbii  1849  3exbii  1850  exanali  1859  exancom  1861  19.43  1882  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1954  exdistr2  1958  3exdistr  1960  19.12vvv  1994  excom13  2165  exrot4  2167  2sb5  2278  dfsb7  2279  eeor  2332  19.12vv  2345  eean  2346  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  equsexALT  2417  2sb5rf  2470  2sb8e  2528  mo4  2559  eu6lem  2566  eubii  2578  sb8eulem  2591  cbvmovw  2595  cbvmow  2596  eu1  2603  sbmo  2607  2moswapv  2622  2moswap  2637  euae  2653  issettru  2806  issetlem  2808  clabel  2874  sbabel  2924  nabbib  3028  rextru  3060  rexbii2  3072  r2exlem  3118  r19.41v  3159  r3ex  3168  r19.41  3233  rexcom4  3256  2ex2rexrot  3265  rexv  3466  cgsex4gOLD  3486  ceqsex2  3492  ceqsex2v  3493  ceqsex3v  3494  gencbvex  3498  spc3egv  3560  spc3gv  3561  ceqsrexv  3612  rexrab2  3662  euxfrw  3683  euxfr  3685  euind  3686  reu6  3688  reu3  3689  2reuswap  3708  2reuswap2  3709  reuind  3715  2reu5lem3  3719  2reu5  3720  2rmoswap  3723  sbcimdv  3813  sbcg  3817  sbccomlemOLD  3824  rmo2  3841  rmoanim  3848  rmoanimALT  3849  rexun  4149  reupick3  4283  euelss  4285  ndisj  4323  inn0f  4324  pssnel  4424  rexsns  4625  exsnrex  4634  snprc  4671  euabsn2  4679  reusn  4681  eusn  4684  elpreqpr  4821  elunirab  4876  uniprg  4877  uniun  4884  uniin  4885  uni0b  4887  uniintsn  4938  iuncom4  4953  dfiun2g  4983  iunn0  5019  iunxiun  5049  disjor  5077  cbvopab2  5171  cbvopab2v  5174  unopab  5175  axrep1  5222  axrep4v  5226  axrep4  5227  axrep4OLD  5228  axrep5  5229  axrep6  5230  axrep6OLD  5231  zfrep4  5235  axsepgfromrep  5236  axnulALT  5246  0ex  5249  vnex  5256  inex1  5259  inuni  5292  axpweq  5293  zfpow  5308  axpow2  5309  vpwex  5319  zfpair  5363  zfpair2  5375  el  5384  eqvinop  5434  copsexgw  5437  copsexg  5438  opabn0  5500  iunopab  5506  dfid2  5520  dfid3  5521  opeliunxp  5690  opeliun2xp  5691  xpiundi  5694  xpiundir  5695  elvvv  5699  csbxp  5723  eliunxp  5784  exopxfr  5790  relop  5797  opelco2g  5814  cnvco  5832  cnvuni  5833  dfdm3  5834  dfrn2  5835  dfrn3  5836  elrng  5838  dfdm4  5842  csbdm  5844  eldm2g  5846  dmun  5857  dmin  5858  dmiun  5860  dmuni  5861  dmopab  5862  dmi  5868  dmep  5870  rnep  5873  dmxp  5875  rnopab  5900  dmcosseq  5923  dmcosseqOLD  5924  dmcosseqOLDOLD  5925  dmres  5967  elsnres  5976  dfima2  6017  elima3  6022  imadmrn  6025  imai  6029  args  6047  rniun  6100  xpdifid  6121  ssrnres  6131  dmsnn0  6160  dmsnopg  6166  cnvresima  6183  mptpreima  6191  dfco2  6198  coundi  6200  coundir  6201  resco  6203  imaco  6204  rnco  6205  coiun  6209  coi1  6215  coass  6218  xpco  6241  elsnxp  6243  dfpo2  6248  dffun5  6500  imadif  6570  brprcneu  6816  brprcneuALT  6817  dffv2  6922  fndmin  6983  fvn0ssdmfun  7012  abrexco  7184  imaiun  7185  isomin  7278  imaeqsexvOLD  7304  dfoprab2  7411  cbvoprab2  7441  zfun  7676  uniex2  7678  uniuni  7702  elxp4  7862  elxp5  7863  fiun  7885  f1iun  7886  f11o  7889  fvresex  7902  opabex3d  7907  opabex3rd  7908  opabex3  7909  abexssex  7912  abexex  7913  oprabrexex2  7920  releldm2  7985  dfopab2  7994  dfoprab3s  7995  fsplit  8057  frxp  8066  suppvalbr  8104  cnvimadfsn  8112  brtpos2  8172  dfrecs3  8302  oarec  8487  oeeu  8528  domen  8894  xpsnen  8985  xpcomco  8991  xpassen  8995  dif1enOLD  9086  inf2  9538  zfinf  9554  axinf2  9555  zfinf2  9557  brttrcl2  9629  ttrcltr  9631  ttrclresv  9632  ttrclselem2  9641  rankuni  9778  scott0  9801  cp  9806  ween  9948  aceq1  10030  aceq0  10031  aceq2  10032  dfac5lem1  10036  dfac5lem2  10037  dfac5lem3  10038  kmlem3  10066  kmlem14  10077  kmlem15  10078  kmlem16  10079  cflem  10158  cflemOLD  10159  cf0  10164  cfval2  10173  cfss  10178  cfslb  10179  fin23lem32  10257  axdc2lem  10361  zfac  10373  ac9  10396  ac9s  10406  axpowndlem3  10512  zfcndrep  10527  zfcndun  10528  zfcndpow  10529  zfcndinf  10531  zfcndac  10532  axgroth5  10737  axgroth2  10738  axgroth6  10741  axgroth3  10744  axgroth4  10745  grothprim  10747  grothtsk  10748  genpass  10922  ltexprlem1  10949  ltexprlem4  10952  supaddc  12110  supadd  12111  supmul1  12112  supmullem2  12114  2rexuz  12819  nnwos  12834  hashgt23el  14349  hashfun  14362  wwlktovfo  14883  xpcogend  14899  cbvsum  15620  cbvsumv  15621  cbvprod  15838  cbvprodv  15839  prodeq1i  15841  iprodmul  15928  maxprmfct  16638  4sqlem12  16886  vdwmc  16908  cshwrepswhash1  17032  imasleval  17463  isacs2  17577  cicsym  17729  gsumval3eu  19801  lidlnz  21167  isbasis2g  22851  tgval2  22859  ntreq0  22980  lmff  23204  cmpfi  23311  is1stc2  23345  1stcelcls  23364  unisngl  23430  isfbas2  23738  elfg  23774  alexsubALTlem3  23952  ustfilxp  24116  metrest  24428  metuel2  24469  restmetu  24474  dchrvmasumlema  27427  elold  27801  lrrecfr  27873  sleadd1  27919  addsuniflem  27931  addsasslem1  27933  addsasslem2  27934  mulsuniflem  28075  addsdilem1  28077  addsdilem2  28078  mulsasslem1  28089  mulsasslem2  28090  renegscl  28385  readdscl  28386  remulscl  28389  istrkg2ld  28423  istrkg3ld  28424  1loopgrvd2  29467  wwlksnextsurj  29863  isgrpo  30459  nmo  32452  reuxfrdf  32453  rexunirn  32454  dmrab  32459  disjorf  32541  fcoinvbr  32567  mpomptxf  32634  fpwrelmapffslem  32688  1arithidom  33487  ordtconnlem1  33893  ddemeas  34205  omssubaddlem  34269  omssubadd  34270  eulerpartlemgvv  34346  bnj89  34690  bnj133  34696  bnj1019  34748  bnj1101  34753  bnj1109  34755  bnj1143  34759  bnj1198  34764  bnj1304  34788  bnj605  34876  bnj607  34885  bnj600  34888  bnj865  34892  bnj916  34902  bnj983  34920  bnj985v  34922  bnj985  34923  bnj996  34925  bnj1033  34938  bnj1083  34947  bnj1090  34948  bnj1093  34949  bnj1110  34951  bnj1128  34959  bnj1145  34962  bnj1171  34969  bnj1172  34970  bnj1174  34972  bnj1176  34974  bnj1186  34976  bnj1189  34978  bnj1253  34986  bnj1279  34987  bnj1371  34998  bnj1374  35000  bnj1312  35027  exdifsn  35048  axreg  35064  axregscl  35065  fineqvrep  35072  fineqvpow  35073  axregs  35076  lfuhgr3  35095  loop1cycl  35112  satfvsucsuc  35340  satf0op  35352  axextprim  35676  axrepprim  35677  axunprim  35678  axpowprim  35679  axregprim  35680  axinfprim  35681  axacprim  35682  dftr6  35726  coep  35727  coepr  35728  dffr5  35729  cnvco1  35734  cnvco2  35735  eldm3  35736  fundmpss  35742  dfdm5  35748  dfrn5  35749  elima4  35751  axextdfeq  35773  19.12b  35777  axextndbi  35780  brtxp  35856  brpprod  35861  brsset  35865  dfon3  35868  brtxpsd  35870  elfix  35879  dffix2  35881  sscoid  35889  dffun10  35890  elfuns  35891  elsingles  35894  snelsingles  35898  dfiota3  35899  brimg  35913  brapply  35914  brcup  35915  brcap  35916  brsuccf  35917  funpartlem  35918  brrestrict  35925  dfrecs2  35926  dfrdg4  35927  sumeq2si  36178  prodeq2si  36180  cbvoprab2vw  36214  cbvoprab23vw  36216  cbvprodvw2  36223  neifg  36347  bj-equsexval  36636  bj-eeanvw  36689  bj-substw  36698  eliminable-abelv  36845  eliminable-abelab  36846  bj-denoteslem  36847  bj-rexvw  36856  bj-csbsnlem  36879  bj-gabima  36916  bj-snsetex  36939  bj-elsngl  36944  bj-snglc  36945  bj-abex  37006  bj-clex  37007  bj-clel3gALT  37024  bj-nul  37032  bj-dfid2ALT  37041  bj-restpw  37068  bj-restuni  37073  bj-dfmpoa  37094  bj-opabco  37164  bj-xpcossxp  37165  bj-imdirco  37166  mptsnunlem  37314  topdifinffinlem  37323  difunieq  37350  wl-dfclab  37572  poimirlem26  37628  ismblfin  37643  itg2addnclem3  37655  itg2addnc  37656  ismgmOLD  37832  sbcexfi  38099  sbccom2lem  38106  eldmres  38247  ecinn0  38323  ineleq  38324  moantr  38334  dmcnvep  38349  rnxrn  38372  rnxrnres  38373  dfcoss2  38392  dfcoss3  38393  cosscnv  38395  coss1cnvres  38396  coss2cnvepres  38397  1cossres  38408  cocossss  38415  rncossdmcoss  38434  eldmcoss2  38438  coss0  38458  cossid  38459  dfssr2  38478  eldmqs1cossres  38639  prtlem16  38850  prter2  38862  islshpat  38998  islpln5  39517  islvol5  39561  pmapglb  39752  polval2N  39888  cdlemftr3  40547  dibelval3  41129  dicelval3  41162  dihglb2  41324  sn-axrep5v  42192  prjspeclsp  42588  euabsn2w  42655  diophrex  42751  onsupmaxb  43215  nnoeomeqom  43288  tfsconcatlem  43312  tfsconcat0i  43321  rp-isfinite6  43494  snen1g  43500  relintab  43559  imaiun1  43627  coiun1  43628  clsk3nimkb  44016  expandexn  44265  ismnuprim  44270  rr-groth  44275  ismnushort  44277  rr-grothshortbi  44279  19.36vv  44359  19.37vv  44361  pm11.58  44366  pm11.6  44368  pm13.192  44386  2sbc5g  44392  iotasbc2  44396  onfrALTlem5  44519  onfrALTlem1  44525  ax6e2nd  44535  2sb5nd  44537  en3lplem2VD  44820  onfrALTlem5VD  44861  relopabVD  44877  ax6e2ndVD  44884  2sb5ndVD  44886  ax6e2ndALT  44906  2sb5ndALT  44908  dfac5prim  44967  brpermmodel  44980  permaxrep  44983  permac8prim  44991  rfcnnnub  45017  stoweidlem34  46019  stoweidlem35  46020  stoweidlem60  46045  smfpimcc  46793  ichexmpl1  47457  sprid  47462  dfgric2  47903  usgrgrtrirex  47938  grlimgrtri  47991  eliunxp2  48322  mosssn2  48805  coxp  48821  istermc  49463  setrec1lem3  49678  elpglem3  49702  eximp-surprise  49773