Theorem exbii 1850

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

Syntax hints:   ↔ wb 206  ∃wex 1781

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

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

This theorem is referenced by:  2exbii  1851  3exbii  1852  exanali  1861  exancom  1863  19.43  1884  19.41vv  1952  19.41vvv  1953  19.41vvvv  1954  exdistr  1956  exdistr2  1960  3exdistr  1962  19.12vvv  1996  excom13  2170  exrot4  2172  2sb5  2285  dfsb7  2286  eeor  2339  19.12vv  2352  eean  2353  eeeanv  2355  ee4anv  2356  ee4anvOLD  2357  2sb8ef  2361  equsexALT  2424  2sb5rf  2477  2sb8e  2535  mo4  2567  eu6lem  2574  sb8eulem  2599  cbvmovw  2603  cbvmow  2604  eu1  2611  sbmo  2615  2moswapv  2630  2moswap  2645  euae  2661  issettru  2815  issetlem  2817  clabel  2882  sbabel  2932  nabbib  3036  rextru  3069  rexbii2  3081  r2exlem  3127  r19.41v  3168  r3ex  3177  r19.41  3242  rexcom4  3265  2ex2rexrot  3273  rexv  3470  cgsex4gOLD  3490  ceqsex2  3495  ceqsex2v  3496  ceqsex3v  3497  gencbvex  3501  spc3egv  3559  spc3gv  3560  ceqsrexv  3611  rexrab2  3660  euxfrw  3681  euxfr  3683  euind  3684  reu6  3686  reu3  3687  2reuswap  3706  2reuswap2  3707  reuind  3713  2reu5lem3  3717  2reu5  3718  2rmoswap  3721  sbcimdv  3811  sbcg  3815  sbccomlemOLD  3822  rmo2  3839  rmoanim  3846  rmoanimALT  3847  rexun  4150  reupick3  4284  euelss  4286  ndisj  4324  inn0f  4325  pssnel  4425  rexsns  4630  exsnrex  4639  snprc  4676  euabsn2  4684  reusn  4686  eusn  4689  elpreqpr  4825  elunirab  4880  uniprg  4881  uniun  4888  uniin  4889  uni0b  4891  uniintsn  4942  iuncom4  4957  dfiun2g  4987  iunn0  5024  iunxiun  5054  disjor  5082  cbvopab2  5176  cbvopab2v  5179  unopab  5180  axrep1  5227  axrep4v  5231  axrep4  5232  axrep4OLD  5233  axrep5  5234  axrep6  5235  axrep6OLD  5236  zfrep4  5240  axsepgfromrep  5241  axnulALT  5251  0ex  5254  vnex  5261  inex1  5264  inuni  5297  axpweq  5298  zfpow  5313  axpow2  5314  vpwex  5324  zfpair  5368  zfpair2  5380  prex  5384  el  5394  eqvinop  5443  copsexgw  5446  copsexg  5447  opabn0  5509  iunopab  5515  dfid2  5529  dfid3  5530  opeliunxp  5699  opeliun2xp  5700  xpiundi  5703  xpiundir  5704  elvvv  5708  csbxp  5733  eliunxp  5794  exopxfr  5800  relop  5807  opelco2g  5824  cnvco  5842  cnvuni  5843  dfdm3  5844  dfrn2  5845  dfrn3  5846  elrng  5848  dfdm4  5852  csbdm  5854  eldm2g  5856  dmun  5867  dmin  5868  dmiun  5870  dmuni  5871  dmopab  5872  dmi  5878  dmep  5880  rnep  5884  dmxp  5886  rnopab  5911  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  dmres  5979  elsnres  5988  dfima2  6029  elima3  6034  imadmrn  6037  imai  6041  args  6059  rniun  6113  xpdifid  6134  ssrnres  6144  dmsnn0  6173  dmsnopg  6179  cnvresima  6196  mptpreima  6204  dfco2  6211  coundi  6213  coundir  6214  resco  6216  imaco  6217  rnco  6218  rncoOLD  6219  coiun  6223  coi1  6229  coass  6232  xpco  6255  elsnxp  6257  dfpo2  6262  dffun5  6514  imadif  6584  tz6.12-2  6829  brprcneu  6832  brprcneuALT  6833  dffv2  6937  fndmin  6999  fvn0ssdmfun  7028  abrexco  7200  imaiun  7201  isomin  7293  imaeqsexvOLD  7319  dfoprab2  7426  cbvoprab2  7456  zfun  7691  uniex2  7693  uniuni  7717  elxp4  7874  elxp5  7875  fiun  7897  f1iun  7898  f11o  7901  fvresex  7914  opabex3d  7919  opabex3rd  7920  opabex3  7921  abexssex  7924  abexex  7925  oprabrexex2  7932  releldm2  7997  dfopab2  8006  dfoprab3s  8007  fsplit  8069  frxp  8078  suppvalbr  8116  cnvimadfsn  8124  brtpos2  8184  dfrecs3  8314  oarec  8499  oeeu  8541  domen  8910  xpsnen  9001  xpcomco  9007  xpassen  9011  inf2  9544  zfinf  9560  axinf2  9561  zfinf2  9563  brttrcl2  9635  ttrcltr  9637  ttrclresv  9638  ttrclselem2  9647  rankuni  9787  scott0  9810  cp  9815  ween  9957  aceq1  10039  aceq0  10040  aceq2  10041  dfac5lem1  10045  dfac5lem2  10046  dfac5lem3  10047  kmlem3  10075  kmlem14  10086  kmlem15  10087  kmlem16  10088  cflem  10167  cflemOLD  10168  cf0  10173  cfval2  10182  cfss  10187  cfslb  10188  fin23lem32  10266  axdc2lem  10370  zfac  10382  ac9  10405  ac9s  10415  axpowndlem3  10522  zfcndrep  10537  zfcndun  10538  zfcndpow  10539  zfcndinf  10541  zfcndac  10542  axgroth5  10747  axgroth2  10748  axgroth6  10751  axgroth3  10754  axgroth4  10755  grothprim  10757  grothtsk  10758  genpass  10932  ltexprlem1  10959  ltexprlem4  10962  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  2rexuz  12825  nnwos  12840  hashgt23el  14359  hashfun  14372  wwlktovfo  14893  xpcogend  14909  cbvsum  15630  cbvsumv  15631  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  iprodmul  15938  maxprmfct  16648  4sqlem12  16896  vdwmc  16918  cshwrepswhash1  17042  imasleval  17474  isacs2  17588  cicsym  17740  gsumval3eu  19845  lidlnz  21209  isbasis2g  22904  tgval2  22912  ntreq0  23033  lmff  23257  cmpfi  23364  is1stc2  23398  1stcelcls  23417  unisngl  23483  isfbas2  23791  elfg  23827  alexsubALTlem3  24005  ustfilxp  24169  metrest  24480  metuel2  24521  restmetu  24526  dchrvmasumlema  27479  elold  27867  lrrecfr  27951  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  mulsuniflem  28157  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  elreno2  28503  renegscl  28506  readdscl  28507  remulscl  28510  istrkg2ld  28544  istrkg3ld  28545  1loopgrvd2  29589  wwlksnextsurj  29985  isgrpo  30584  nmo  32575  reuxfrdf  32576  rexunirn  32577  dmrab  32582  disjorf  32665  fcoinvbr  32691  mpomptxf  32767  fpwrelmapffslem  32821  1arithidom  33629  ordtconnlem1  34101  ddemeas  34413  omssubaddlem  34476  omssubadd  34477  eulerpartlemgvv  34553  bnj89  34897  bnj133  34903  bnj1019  34955  bnj1101  34960  bnj1109  34962  bnj1143  34965  bnj1198  34970  bnj1304  34994  bnj605  35082  bnj607  35091  bnj600  35094  bnj865  35098  bnj916  35108  bnj983  35126  bnj985v  35128  bnj985  35129  bnj996  35131  bnj1033  35144  bnj1083  35153  bnj1090  35154  bnj1093  35155  bnj1110  35157  bnj1128  35165  bnj1145  35168  bnj1171  35175  bnj1172  35176  bnj1174  35178  bnj1176  35180  bnj1186  35182  bnj1189  35184  bnj1253  35192  bnj1279  35193  bnj1371  35204  bnj1374  35206  bnj1312  35233  exdifsn  35254  fineqvrep  35289  fineqvpow  35290  axreg  35302  axregscl  35303  axregs  35314  lfuhgr3  35333  loop1cycl  35350  satfvsucsuc  35578  satf0op  35590  axextprim  35914  axrepprim  35915  axunprim  35916  axpowprim  35917  axregprim  35918  axinfprim  35919  axacprim  35920  dftr6  35964  coep  35965  coepr  35966  dffr5  35967  cnvco1  35972  cnvco2  35973  eldm3  35974  fundmpss  35980  dfdm5  35986  dfrn5  35987  elima4  35989  axextdfeq  36008  19.12b  36012  axextndbi  36015  brtxp  36091  brpprod  36096  brsset  36100  dfon3  36103  brtxpsd  36105  elfix  36114  dffix2  36116  sscoid  36124  dffun10  36125  elfuns  36126  elsingles  36129  snelsingles  36133  dfiota3  36134  brimg  36148  brapply  36149  brcup  36150  brcap  36151  lemsuccf  36152  funpartlem  36155  brrestrict  36162  dfrecs2  36163  dfrdg4  36164  sumeq2si  36415  prodeq2si  36417  cbvoprab2vw  36451  cbvoprab23vw  36453  cbvprodvw2  36460  neifg  36584  regsfromregtr  36687  regsfromunir1  36689  bj-df-sb  36894  bj-equsexval  36902  bj-eeanvw  36955  bj-substw  36965  eliminable-abelv  37114  eliminable-abelab  37115  bj-denoteslem  37116  bj-rexvw  37125  bj-csbsnlem  37148  bj-gabima  37185  bj-snsetex  37208  bj-elsngl  37213  bj-snglc  37214  bj-abex  37275  bj-clex  37276  bj-clel3gALT  37293  bj-nul  37301  bj-dfid2ALT  37310  bj-rep  37318  bj-axseprep  37319  bj-restpw  37342  bj-restuni  37347  bj-dfmpoa  37368  bj-opabco  37440  bj-xpcossxp  37441  bj-imdirco  37442  mptsnunlem  37590  topdifinffinlem  37599  difunieq  37626  wl-dfclab  37837  poimirlem26  37894  ismblfin  37909  itg2addnclem3  37921  itg2addnc  37922  ismgmOLD  38098  sbcexfi  38365  sbccom2lem  38372  eldmres  38525  ecinn0  38601  ineleq  38602  moantr  38620  dmcnvep  38636  rnxrn  38669  rnxrnres  38670  dmsucmap  38716  dfcoss2  38751  dfcoss3  38752  cosscnv  38754  coss1cnvres  38755  coss2cnvepres  38756  1cossres  38767  cocossss  38774  rncossdmcoss  38793  eldmcoss2  38797  coss0  38817  cossid  38818  dfssr2  38827  eldmqs1cossres  38992  prtlem16  39242  prter2  39254  islshpat  39390  islpln5  39908  islvol5  39952  pmapglb  40143  polval2N  40279  cdlemftr3  40938  dibelval3  41520  dicelval3  41553  dihglb2  41715  sn-axrep5v  42586  prjspeclsp  42967  euabsn2w  43034  diophrex  43129  onsupmaxb  43593  nnoeomeqom  43666  tfsconcatlem  43690  tfsconcat0i  43699  rp-isfinite6  43871  snen1g  43877  relintab  43936  imaiun1  44004  coiun1  44005  clsk3nimkb  44393  expandexn  44642  ismnuprim  44647  rr-groth  44652  ismnushort  44654  rr-grothshortbi  44656  19.36vv  44736  19.37vv  44738  pm11.58  44743  pm11.6  44745  pm13.192  44763  2sbc5g  44769  iotasbc2  44773  onfrALTlem5  44895  onfrALTlem1  44901  ax6e2nd  44911  2sb5nd  44913  en3lplem2VD  45196  onfrALTlem5VD  45237  relopabVD  45253  ax6e2ndVD  45260  2sb5ndVD  45262  ax6e2ndALT  45282  2sb5ndALT  45284  dfac5prim  45343  brpermmodel  45356  permaxrep  45359  permac8prim  45367  rfcnnnub  45393  stoweidlem34  46389  stoweidlem35  46390  stoweidlem60  46415  smfpimcc  47163  ichexmpl1  47826  sprid  47831  dfgric2  48272  usgrgrtrirex  48307  grlimgrtri  48360  eliunxp2  48691  mosssn2  49173  coxp  49189  istermc  49830  setrec1lem3  50045  elpglem3  50069  eximp-surprise  50140