Theorem exbii 1880

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  2exbii  1881  3exbii  1882  exanali  1891  exancom  1893  19.43  1914  19.41vv  1982  19.41vvv  1983  19.41vvvv  1984  exdistr  1986  exdistr2  1990  3exdistr  1992  19.12vvv  2026  excom13  2200  exrot4  2202  2sb5  2311  dfsb7  2312  eeor  2363  19.12vv  2376  eean  2377  eeeanv  2379  ee4anv  2380  ee4anvOLD  2381  2sb8ef  2385  equsexALT  2448  2sb5rf  2501  2sb8e  2559  mo4  2591  eu6lem  2598  sb8eulem  2623  cbvmovw  2627  cbvmow  2628  eu1  2635  sbmo  2639  2moswapv  2654  2moswap  2669  euae  2684  issettru  2838  issetlem  2840  clabel  2905  sbabel  2954  nabbib  3060  rextru  3093  rexbii2  3105  r2exlem  3151  r19.41v  3192  r3ex  3201  r19.41  3266  rexcom4  3289  2ex2rexrot  3297  rexv  3477  ceqsex2  3500  ceqsex2v  3501  ceqsex3v  3502  gencbvex  3506  spc3egv  3557  spc3gv  3558  ceqsrexv  3608  rexrab2  3657  euxfrw  3678  euxfr  3680  euind  3681  reu6  3683  reu3  3684  2reuswap  3703  2reuswap2  3704  reuind  3710  2reu5lem3  3714  2reu5  3715  2rmoswap  3718  sbcimdv  3806  sbcg  3810  rmo2  3833  rmoanim  3841  rmoanimALT  3842  rexun  4194  reupick3  4275  euelss  4277  ndisj  4317  inn0f  4318  pssnel  4423  rexsns  4628  exsnrex  4637  snprc  4674  euabsn2  4682  reusn  4684  eusn  4687  elpreqpr  4821  elunirab  4881  uniprg  4882  uniun  4889  uniinOLD  4891  uni0b  4893  uniintsn  4944  iuncom4  4959  dfiun2g  4987  iunn0  5024  iunxiun  5056  disjor  5084  cbvopab2  5180  cbvopab2v  5183  unopab  5184  axrep1  5232  axrep4v  5236  axrep4  5237  axrep5  5238  axrep6  5239  zfrep6  5241  zfrep4  5245  axsepgfromrep  5246  axnulALT  5257  0ex  5260  vnexOLD  5271  inex1  5276  inuni  5310  axpweq  5311  zfpow  5327  axpow2  5328  vpwex  5338  zfpair  5382  zfpair2  5391  prex  5395  el.OLD  5406  eqvinop  5455  eqvinot  5456  copsexgw  5459  copsexgwOLD  5460  copsexg  5461  cotsexgw  5462  opabn0  5527  iunopab  5533  dfid2  5547  dfid3  5548  opeliunxp  5717  opeliun2xp  5718  xpiundi  5721  xpiundir  5722  elvvv  5726  csbxp  5751  eliunxp  5813  exopxfr  5820  relop  5827  opelco2g  5844  cnvco  5866  cnvuni  5867  dfdm3  5868  dfrn2  5869  dfrn3  5870  elrng  5872  dfdm4  5876  csbdm  5878  eldm2g  5880  dmun  5891  dmin  5892  dmiun  5894  dmuni  5895  dmopab  5896  dmi  5902  dmep  5904  rnep  5908  dmxp  5910  rnopab  5935  dmcosseq  5959  dmcosseqOLD  5960  dmres  6002  elsnres  6009  dfima2  6057  elima3  6062  imadmrnOLD  6067  imai  6071  args  6089  rniun  6138  xpdifid  6158  xpdifcnvepel  6159  ssrnres  6169  dmsnn0  6208  dmsnopg  6214  cnvresima  6231  mptpreima  6239  dfco2  6246  coundi  6248  coundir  6249  resco  6251  imaco  6252  rnco  6253  rncoOLD  6254  coiun  6258  coi1  6264  coass  6267  xpco  6292  elsnxp  6294  dfpo2  6299  dffun5  6553  imadif  6625  tz6.12-2  6873  brprcneu  6876  brprcneuALT  6877  dffv2  6981  fndmin  7045  fvn0ssdmfun  7075  abrexco  7249  imaiun  7250  isomin  7346  dfoprab2  7479  cbvoprab2  7509  zfun  7753  uniex2  7755  uniex2OLD  7756  uniuni  7777  elxp4  7935  elxp5  7936  fiun  7956  f1iun  7957  f11o  7960  fvresex  7973  opabex3d  7978  opabex3rd  7979  opabex3  7980  abexssex  7983  abexex  7984  oprabrexex2  7991  releldm2  8055  dfopab2  8064  dfoprab3s  8065  fsplit  8131  frxp  8141  suppvalbr  8184  suppvalbrOLD  8185  cnvimadfsn  8193  brtpos2  8253  dfrecs3  8384  oarec  8574  oeeu  8616  domen  8992  xpsnen  9084  xpcomco  9090  xpassen  9094  inf2  9628  zfinf  9644  axinf2  9645  zfinf2  9647  brttrcl2  9719  ttrcltr  9721  ttrclresv  9722  ttrclselem2  9731  rankuni  9883  scott0b  9941  scott0OLD  9942  cp  9958  setrec1lem3  9973  ween  10118  aceq1  10200  aceq0  10201  aceq2  10202  dfac5lem1  10206  dfac5lem2  10207  dfac5lem3  10208  kmlem3  10235  kmlem14  10246  kmlem15  10247  kmlem16  10248  cflem  10327  cf0  10332  cfval2  10342  cfss  10347  cfslb  10348  fin23lem32  10426  axdc2lem  10530  zfac  10542  ac9  10565  ac9s  10575  axpowndlem3  10688  zfcndrep  10703  zfcndun  10704  zfcndpow  10705  zfcndinf  10707  zfcndac  10708  axgroth5  10913  axgroth2  10914  axgroth6  10917  axgroth3  10920  axgroth4  10921  grothprim  10923  grothtsk  10924  genpass  11098  ltexprlem1  11125  ltexprlem4  11128  supaddc  12288  supadd  12289  supmul1  12290  supmullem2  12292  2rexuz  13031  nnwos  13046  hashgt23el  14573  hashfun  14586  wwlktovfo  15117  xpcogend  15133  cbvsum  15868  cbvsumv  15869  cbvprod  16088  cbvprodv  16089  prodeq1i  16091  iprodmul  16176  maxprmfct  16891  4sqlem12  17140  vdwmc  17162  cshwrepswhash1  17286  imasleval  17719  isacs2  17833  cicsym  17985  gsumval3eu  20124  lidlnz  21536  isbasis2g  23272  tgval2  23280  ntreq0  23401  lmff  23625  cmpfi  23732  is1stc2  23766  1stcelcls  23786  unisngl  23852  isfbas2  24160  elfg  24196  alexsubALTlem3  24374  ustfilxp  24538  metrest  24849  metuel2  24890  restmetu  24895  dchrvmasumlema  27833  elold  28251  lrrecfr  28335  leadds1  28381  addsuniflem  28393  addsasslem1  28395  addsasslem2  28396  mulsuniflem  28541  addsdilem1  28543  addsdilem2  28544  mulsasslem1  28555  mulsasslem2  28556  elreno2  28887  renegscl  28890  readdscl  28891  remulscl  28894  istrkg2ld  28928  istrkg3ld  28929  lfuhgr3  29734  1loopgrvd2  30090  wwlksnextsurj  30495  loop1cycl  30750  isgrpo  31105  nmo  33134  reuxfrdf  33135  rexunirn  33136  dmrab  33141  disjorf  33221  fcoinvbr  33247  mpomptxf  33320  fpwrelmapffslem  33371  1arithidom  34116  ordtconnlem1  34603  ddemeas  34916  omssubaddlem  34978  omssubadd  34979  eulerpartlemgvv  35055  bnj89  35399  bnj133  35405  bnj1019  35457  bnj1101  35462  bnj1109  35464  bnj1143  35467  bnj1198  35472  bnj1304  35496  bnj605  35584  bnj607  35593  bnj600  35596  bnj865  35600  bnj916  35610  bnj983  35628  bnj985v  35630  bnj985  35631  bnj996  35633  bnj1033  35646  bnj1083  35655  bnj1090  35656  bnj1093  35657  bnj1110  35659  bnj1128  35667  bnj1145  35670  bnj1171  35677  bnj1172  35678  bnj1174  35680  bnj1176  35682  bnj1186  35684  bnj1189  35686  bnj1253  35694  bnj1279  35695  bnj1371  35706  bnj1374  35708  bnj1312  35735  reu6f  35756  exdifsn  35760  axnulALT2  35761  axprALT2  35787  fineqvrep  35839  fineqvpow  35840  axreg  35852  axregscl  35853  axregs  35864  axpowg  35871  onvfowev  35970  vsmrep  36010  satfvsucsuc  36217  satf0op  36229  axextprim  36559  axrepprim  36560  axunprim  36561  axpowprim  36562  axregprim  36563  axinfprim  36564  axacprim  36565  dftr6  36609  coep  36610  coepr  36611  dffr5  36612  cnvco1  36617  cnvco2  36618  eldm3  36619  fundmpss  36625  dfdm5  36630  dfrn5  36631  elima4  36633  axextdfeq  36652  19.12b  36656  axextndbi  36659  brtxp  36735  brpprod  36740  brsset  36744  dfon3  36747  brtxpsd  36749  elfix  36758  dffix2  36760  sscoid  36768  dffun10  36769  elfuns  36770  elsingles  36773  snelsingles  36777  dfiota3  36778  brimg  36792  brapply  36793  brcup  36794  brcap  36795  lemsuccf  36796  funpartlem  36799  brrestrict  36806  dfrecs2  36807  dfrdg4  36808  sumeq2si  37084  prodeq2si  37086  cbvoprab2vw  37120  cbvoprab23vw  37122  cbvprodvw2  37129  neifg  37252  regsfromregtco  37419  regsfromunir1  37421  mh-prprimbi  37424  mh-unprimbi  37425  mh-infprim1bi  37427  mh-infprim2bi  37428  mh-infprim3bi  37429  bj-df-sb  37642  bj-dfsbc  37644  bj-equsexval  37652  bj-eeanvw  37710  bj-substw  37720  eliminable-abelv  37874  eliminable-abelab  37875  bj-denoteslem  37876  bj-rexvw  37885  bj-csbsnlem  37908  bj-gabima  37946  bj-snsetex  37969  bj-elsngl  37974  bj-snglc  37975  bj-abex  38036  bj-clex  38037  coi1in  38054  bj-clel3gALT  38056  bj-nul  38064  bj-dfid2ALT  38073  bj-rep  38082  bj-axseprep  38083  bj-restpw  38106  bj-restuni  38111  bj-dfmpoa  38133  bj-opabco  38203  bj-xpcossxp  38204  bj-imdirco  38205  mptsnunlem  38355  topdifinffinlem  38364  difunieq  38391  wl-dfclab  38611  poimirlem26  38658  ismblfin  38673  itg2addnclem3  38685  itg2addnc  38686  negprop  38737  impprop  38738  ismgmOLD  38878  sbcexfi  39143  sbccom2lem  39150  eldmres  39303  ecinn0  39379  ineleq  39380  moantr  39398  dmcnvep  39414  rnxrn  39447  rnxrnres  39448  dmsucmap  39494  dfcoss2  39529  dfcoss3  39530  cosscnv  39532  coss1cnvres  39533  coss2cnvepres  39534  1cossres  39545  cocossss  39552  rncossdmcoss  39571  eldmcoss2  39575  coss0  39595  cossid  39596  dfssr2  39605  eldmqs1cossres  39770  prtlem16  40020  prter2  40032  islshpat  40168  islpln5  40686  islvol5  40730  pmapglb  40921  polval2N  41057  cdlemftr3  41716  dibelval3  42298  dicelval3  42331  dihglb2  42493  sn-axrep5v  43365  prjspeclsp  43734  euabsn2w  43784  diophrex  43880  onsupmaxb  44335  nnoeomeqom  44408  tfsconcatlem  44432  tfsconcat0i  44441  rp-isfinite6  44613  snen1g  44619  relintab  44678  imaiun1  44745  coiun1  44746  clsk3nimkb  45134  expandexn  45367  ismnuprim  45372  rr-groth  45377  ismnushort  45379  rr-grothshortbi  45381  19.36vv  45461  19.37vv  45463  pm11.58  45468  pm11.6  45470  pm13.192  45488  2sbc5g  45494  iotasbc2  45498  onfrALTlem5  45619  onfrALTlem1  45625  ax6e2nd  45635  2sb5nd  45637  en3lplem2VD  45920  onfrALTlem5VD  45961  relopabVD  45977  ax6e2ndVD  45984  2sb5ndVD  45986  ax6e2ndALT  46006  2sb5ndALT  46008  dfac5prim  46074  brpermmodel  46087  permaxrep  46090  permac8prim  46098  rfcnnnub  46147  stoweidlem34  47138  stoweidlem35  47139  stoweidlem60  47164  smfpimcc  47912  ichexmpl1  48645  sprid  48650  dfgric2  49107  usgrgrtrirex  49142  grlimgrtri  49195  eliunxp2  49540  mosssn2  50022  coxp  50038  istermc  50703  elpglem3  50975  eximp-surprise  51049  alsbii  51065