Theorem exbii 1856

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

Syntax hints:   ↔ wb 208  ∃wex 1787

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

This theorem depends on definitions:  df-bi 209  df-ex 1788

This theorem is referenced by:  2exbii  1857  3exbii  1858  exanali  1867  exancom  1869  19.43  1890  19.41vv  1958  19.41vvv  1959  19.41vvvv  1960  exdistr  1962  exdistr2  1966  3exdistr  1968  19.12vvv  2002  excom13  2177  exrot4  2179  2sb5  2291  dfsb7  2292  eeor  2344  19.12vv  2357  eean  2358  eeeanv  2360  ee4anv  2361  ee4anvOLD  2362  2sb8ef  2366  equsexALT  2429  2sb5rf  2482  2sb8e  2540  mo4  2572  eu6lem  2579  sb8eulem  2604  cbvmovw  2608  cbvmow  2609  eu1  2616  sbmo  2620  2moswapv  2635  2moswap  2650  euae  2665  issettru  2819  issetlem  2821  clabel  2886  sbabel  2935  nabbib  3039  rextru  3072  rexbii2  3084  r2exlem  3130  r19.41v  3171  r3ex  3180  r19.41  3245  rexcom4  3268  2ex2rexrot  3276  rexv  3460  ceqsex2  3483  ceqsex2v  3484  ceqsex3v  3485  gencbvex  3489  spc3egv  3542  spc3gv  3543  ceqsrexv  3594  rexrab2  3642  euxfrw  3663  euxfr  3665  euind  3666  reu6  3668  reu3  3669  2reuswap  3688  2reuswap2  3689  reuind  3695  2reu5lem3  3699  2reu5  3700  2rmoswap  3703  sbcimdv  3792  sbcg  3796  sbccomlemOLD  3803  rmo2  3820  rmoanim  3827  rmoanimALT  3828  rexun  4127  reupick3  4260  euelss  4262  ndisj  4300  inn0f  4301  pssnel  4401  rexsns  4605  exsnrex  4614  snprc  4651  euabsn2  4659  reusn  4661  eusn  4664  elpreqpr  4800  elunirab  4855  uniprg  4856  uniun  4863  uniin  4864  uni0b  4866  uniintsn  4917  iuncom4  4932  dfiun2g  4961  iunn0  4998  iunxiun  5028  disjor  5056  cbvopab2  5150  cbvopab2v  5153  unopab  5154  axrep1  5202  axrep4v  5206  axrep4  5207  axrep4OLD  5208  axrep5  5209  axrep6  5210  axrep6OLD  5211  zfrep6  5213  zfrep4  5217  axsepgfromrep  5218  axnulALT  5228  0ex  5231  vnexOLD  5242  inex1  5247  inuni  5280  axpweq  5281  zfpow  5297  axpow2  5298  vpwex  5308  zfpair  5352  zfpair2  5365  prex  5369  elOLD  5380  eqvinop  5429  copsexgw  5432  copsexgwOLD  5433  copsexg  5434  opabn0  5497  iunopab  5503  dfid2  5517  dfid3  5518  opeliunxp  5687  opeliun2xp  5688  xpiundi  5691  xpiundir  5692  elvvv  5696  csbxp  5721  eliunxp  5781  exopxfr  5787  relop  5794  opelco2g  5811  cnvco  5833  cnvuni  5834  dfdm3  5835  dfrn2  5836  dfrn3  5837  elrng  5839  dfdm4  5843  csbdm  5845  eldm2g  5847  dmun  5858  dmin  5859  dmiun  5861  dmuni  5862  dmopab  5863  dmi  5869  dmep  5871  rnep  5875  dmxp  5877  rnopab  5902  dmcosseq  5926  dmcosseqOLD  5927  dmcosseqOLDOLD  5928  dmres  5970  elsnres  5979  dfima2  6020  elima3  6025  imadmrn  6028  imai  6032  args  6050  rniun  6101  xpdifid  6122  ssrnres  6132  dmsnn0  6161  dmsnopg  6167  cnvresima  6184  mptpreima  6192  dfco2  6199  coundi  6201  coundir  6202  resco  6204  imaco  6205  rnco  6206  rncoOLD  6207  coiun  6211  coi1  6217  coass  6220  xpco  6243  elsnxp  6245  dfpo2  6250  dffun5  6502  imadif  6572  tz6.12-2  6817  brprcneu  6820  brprcneuALT  6821  dffv2  6925  fndmin  6989  fvn0ssdmfun  7018  abrexco  7191  imaiun  7192  isomin  7284  imaeqsexvOLD  7310  dfoprab2  7417  cbvoprab2  7447  zfun  7682  uniex2  7684  uniuni  7708  elxp4  7866  elxp5  7867  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  8058  frxp  8068  suppvalbr  8106  cnvimadfsn  8114  brtpos2  8174  dfrecs3  8305  oarec  8491  oeeu  8533  domen  8902  xpsnen  8993  xpcomco  8999  xpassen  9003  inf2  9539  zfinf  9555  axinf2  9556  zfinf2  9558  brttrcl2  9630  ttrcltr  9632  ttrclresv  9633  ttrclselem2  9642  rankuni  9782  scott0  9805  cp  9810  ween  9952  aceq1  10034  aceq0  10035  aceq2  10036  dfac5lem1  10040  dfac5lem2  10041  dfac5lem3  10042  kmlem3  10070  kmlem14  10081  kmlem15  10082  kmlem16  10083  cflem  10162  cflemOLD  10163  cf0  10168  cfval2  10178  cfss  10183  cfslb  10184  fin23lem32  10262  axdc2lem  10366  zfac  10378  ac9  10401  ac9s  10411  axpowndlem3  10518  zfcndrep  10533  zfcndun  10534  zfcndpow  10535  zfcndinf  10537  zfcndac  10538  axgroth5  10743  axgroth2  10744  axgroth6  10747  axgroth3  10750  axgroth4  10751  grothprim  10753  grothtsk  10754  genpass  10928  ltexprlem1  10955  ltexprlem4  10958  supaddc  12118  supadd  12119  supmul1  12120  supmullem2  12122  2rexuz  12845  nnwos  12860  hashgt23el  14381  hashfun  14394  wwlktovfo  14915  xpcogend  14931  cbvsum  15652  cbvsumv  15653  cbvprod  15873  cbvprodv  15874  prodeq1i  15876  iprodmul  15963  maxprmfct  16674  4sqlem12  16922  vdwmc  16944  cshwrepswhash1  17068  imasleval  17500  isacs2  17614  cicsym  17766  gsumval3eu  19873  lidlnz  21238  isbasis2g  22934  tgval2  22942  ntreq0  23063  lmff  23287  cmpfi  23394  is1stc2  23428  1stcelcls  23447  unisngl  23513  isfbas2  23821  elfg  23857  alexsubALTlem3  24035  ustfilxp  24199  metrest  24510  metuel2  24551  restmetu  24556  dchrvmasumlema  27484  elold  27871  lrrecfr  27955  leadds1  28001  addsuniflem  28013  addsasslem1  28015  addsasslem2  28016  mulsuniflem  28161  addsdilem1  28163  addsdilem2  28164  mulsasslem1  28175  mulsasslem2  28176  elreno2  28507  renegscl  28510  readdscl  28511  remulscl  28514  istrkg2ld  28548  istrkg3ld  28549  1loopgrvd2  29592  wwlksnextsurj  29988  isgrpo  30588  nmo  32579  reuxfrdf  32580  rexunirn  32581  dmrab  32586  disjorf  32670  fcoinvbr  32696  mpomptxf  32772  fpwrelmapffslem  32826  1arithidom  33630  ordtconnlem1  34118  ddemeas  34430  omssubaddlem  34493  omssubadd  34494  eulerpartlemgvv  34570  bnj89  34917  bnj133  34923  bnj1019  34975  bnj1101  34980  bnj1109  34982  bnj1143  34985  bnj1198  34990  bnj1304  35014  bnj605  35102  bnj607  35111  bnj600  35114  bnj865  35118  bnj916  35128  bnj983  35146  bnj985v  35148  bnj985  35149  bnj996  35151  bnj1033  35164  bnj1083  35173  bnj1090  35174  bnj1093  35175  bnj1110  35177  bnj1128  35185  bnj1145  35188  bnj1171  35195  bnj1172  35196  bnj1174  35198  bnj1176  35200  bnj1186  35202  bnj1189  35204  bnj1253  35212  bnj1279  35213  bnj1371  35224  bnj1374  35226  bnj1312  35253  exdifsn  35274  axnulALT2  35277  axprALT2  35303  fineqvrep  35308  fineqvpow  35309  axreg  35321  axregscl  35322  axregs  35333  axpowg  35340  lfuhgr3  35361  loop1cycl  35378  satfvsucsuc  35606  satf0op  35618  axextprim  35942  axrepprim  35943  axunprim  35944  axpowprim  35945  axregprim  35946  axinfprim  35947  axacprim  35948  dftr6  35992  coep  35993  coepr  35994  dffr5  35995  cnvco1  36000  cnvco2  36001  eldm3  36002  fundmpss  36008  dfdm5  36014  dfrn5  36015  elima4  36017  axextdfeq  36036  19.12b  36040  axextndbi  36043  brtxp  36119  brpprod  36124  brsset  36128  dfon3  36131  brtxpsd  36133  elfix  36142  dffix2  36144  sscoid  36152  dffun10  36153  elfuns  36154  elsingles  36157  snelsingles  36161  dfiota3  36162  brimg  36176  brapply  36177  brcup  36178  brcap  36179  lemsuccf  36180  funpartlem  36183  brrestrict  36190  dfrecs2  36191  dfrdg4  36192  sumeq2si  36443  prodeq2si  36445  cbvoprab2vw  36479  cbvoprab23vw  36481  cbvprodvw2  36488  neifg  36612  regsfromregtco  36779  regsfromunir1  36781  mh-prprimbi  36784  mh-unprimbi  36785  mh-infprim1bi  36787  mh-infprim2bi  36788  mh-infprim3bi  36789  bj-df-sb  37003  bj-dfsbc  37005  bj-equsexval  37013  bj-eeanvw  37071  bj-substw  37081  eliminable-abelv  37235  eliminable-abelab  37236  bj-denoteslem  37237  bj-rexvw  37246  bj-csbsnlem  37269  bj-gabima  37306  bj-snsetex  37329  bj-elsngl  37334  bj-snglc  37335  bj-abex  37396  bj-clex  37397  bj-clel3gALT  37414  bj-nul  37422  bj-dfid2ALT  37431  bj-rep  37439  bj-axseprep  37440  bj-restpw  37463  bj-restuni  37468  bj-dfmpoa  37489  bj-opabco  37561  bj-xpcossxp  37562  bj-imdirco  37563  mptsnunlem  37713  topdifinffinlem  37722  difunieq  37749  wl-dfclab  37969  poimirlem26  38026  ismblfin  38041  itg2addnclem3  38053  itg2addnc  38054  ismgmOLD  38230  sbcexfi  38497  sbccom2lem  38504  eldmres  38657  ecinn0  38733  ineleq  38734  moantr  38752  dmcnvep  38768  rnxrn  38801  rnxrnres  38802  dmsucmap  38848  dfcoss2  38883  dfcoss3  38884  cosscnv  38886  coss1cnvres  38887  coss2cnvepres  38888  1cossres  38899  cocossss  38906  rncossdmcoss  38925  eldmcoss2  38929  coss0  38949  cossid  38950  dfssr2  38959  eldmqs1cossres  39124  prtlem16  39374  prter2  39386  islshpat  39522  islpln5  40040  islvol5  40084  pmapglb  40275  polval2N  40411  cdlemftr3  41070  dibelval3  41652  dicelval3  41685  dihglb2  41847  sn-axrep5v  42717  prjspeclsp  43075  euabsn2w  43142  diophrex  43237  onsupmaxb  43697  nnoeomeqom  43770  tfsconcatlem  43794  tfsconcat0i  43803  rp-isfinite6  43975  snen1g  43981  relintab  44040  imaiun1  44108  coiun1  44109  clsk3nimkb  44497  expandexn  44746  ismnuprim  44751  rr-groth  44756  ismnushort  44758  rr-grothshortbi  44760  19.36vv  44840  19.37vv  44842  pm11.58  44847  pm11.6  44849  pm13.192  44867  2sbc5g  44873  iotasbc2  44877  onfrALTlem5  44999  onfrALTlem1  45005  ax6e2nd  45015  2sb5nd  45017  en3lplem2VD  45300  onfrALTlem5VD  45341  relopabVD  45357  ax6e2ndVD  45364  2sb5ndVD  45366  ax6e2ndALT  45386  2sb5ndALT  45388  dfac5prim  45447  brpermmodel  45460  permaxrep  45463  permac8prim  45471  rfcnnnub  45497  stoweidlem34  46489  stoweidlem35  46490  stoweidlem60  46515  smfpimcc  47263  ichexmpl1  47956  sprid  47961  dfgric2  48418  usgrgrtrirex  48453  grlimgrtri  48506  eliunxp2  48837  mosssn2  49319  coxp  49335  istermc  49976  setrec1lem3  50191  elpglem3  50215  eximp-surprise  50286