Theorem exbii 1829

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

Syntax hints:   ↔ wb 207  ∃wex 1761

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

This theorem depends on definitions:  df-bi 208  df-ex 1762

This theorem is referenced by:  2exbii  1830  3exbii  1831  exanali  1840  exancom  1842  19.43  1864  19.41vv  1928  19.41vvv  1929  19.41vvvv  1930  exdistr  1932  exdistr2  1936  19.42vvvOLD  1938  3exdistr  1939  19.12vvv  1972  equsexvwOLD  1989  excom13  2135  exrot4  2137  equsexv  2232  2sb5  2245  dfsb7  2251  dfsb7OLD  2252  eeor  2316  19.12vv  2324  eean  2325  eeeanv  2327  ee4anv  2328  2sb8ev  2331  2sb8evOLD  2332  equsexALT  2397  2sb5rf  2453  2sb8e  2530  mo4  2607  eu6lem  2616  eu6OLDOLD  2620  eubii  2630  sb8eulem  2650  eu1  2659  eu1OLD  2660  sbmo  2666  2moswapv  2684  2moswap  2699  euae  2717  euaeOLD  2718  clabel  2931  sbabel  2983  nabbi  3089  rexbii2  3209  rexcom4  3213  2ex2rexrot  3214  rexanidOLD  3217  r2exlem  3265  r19.41v  3308  r19.41  3309  rexcom  3316  isset  3449  rexv  3463  cgsex4g  3482  ceqsex2  3486  ceqsex2v  3487  ceqsex3v  3488  gencbvex  3492  vtocl2OLD  3505  spc3egv  3546  spc3gv  3547  ceqsrexv  3587  rexab  3624  rexrab2  3629  euxfr  3648  euind  3649  reu6  3651  reu3  3652  2reuswap  3671  2reuswap2  3672  reuind  3678  2reu5lem3  3682  2reu5  3683  2rmoswap  3686  sbccomlem  3781  rmo2  3798  rmoanim  3806  rmoanimALT  3807  rexun  4087  reupick3  4208  euelss  4210  ndisj  4247  abn0  4256  pssnel  4334  rexsns  4514  exsnrex  4525  snprc  4560  euabsn2  4568  reusn  4570  eusn  4573  elpreqpr  4704  elunirab  4757  unipr  4758  uniun  4764  uniin  4765  uni0b  4770  uniintsn  4819  iuncom4  4833  dfiun2g  4858  dfiun2gOLD  4859  iunn0  4888  iunxiun  4918  disjor  4944  cbvopab2  5036  cbvopab2v  5039  unopab  5040  axrep1  5082  axrep4  5086  axrep5  5087  axrep6  5088  zfrep4  5091  axsepgfromrep  5092  axnulALT  5099  0ex  5102  vnex  5109  inex1  5112  inuni  5137  axpweq  5156  zfpow  5158  axpow2  5159  axpow3  5160  vpwex  5169  zfpair  5213  zfpair2  5222  eqvinop  5270  copsexg  5273  opabn0  5328  iunopab  5334  dfid3  5349  opeliunxp  5505  xpiundi  5508  xpiundir  5509  elvvv  5513  csbxp  5536  eliunxp  5594  exopxfr  5600  relop  5607  opelco2g  5624  cnvco  5642  cnvuni  5643  dfdm3  5644  dfrn2  5645  dfrn3  5646  elrng  5648  dfdm4  5650  csbdm  5652  eldm2g  5654  dmun  5665  dmin  5666  dmiun  5668  dmuni  5669  dmopab  5670  dmi  5677  elrn  5704  rnopab  5708  dmcosseq  5725  dmres  5756  elsnres  5773  dfima2  5808  elima3  5813  imadmrn  5816  imai  5818  args  5833  rniun  5882  xpdifid  5901  ssrnres  5911  dmsnn0  5939  dmsnopg  5945  cnvresima  5962  mptpreima  5967  dfco2  5973  coundi  5975  coundir  5976  resco  5978  imaco  5979  rnco  5980  coiun  5984  coi1  5990  coass  5993  xpco  6015  elsnxp  6017  dffun2  6235  dffun5  6238  imadif  6308  funimaexg  6310  brprcneu  6530  dffv2  6623  fndmin  6680  fvn0ssdmfun  6707  abrexco  6868  imaiun  6869  isomin  6953  dfoprab2  7071  cbvoprab2  7098  zfun  7320  uniex2  7322  uniuni  7341  elxp4  7483  elxp5  7484  fiun  7500  f1iun  7501  f11o  7504  fvresex  7517  opabex3d  7522  opabex3rd  7523  opabex3  7524  abexssex  7527  abexex  7528  oprabrexex2  7535  releldm2  7598  dfopab2  7606  dfoprab3s  7607  fsplit  7668  frxp  7673  suppvalbr  7685  cnvimadfsn  7690  brtpos2  7749  wfrfun  7817  dfrecs3  7861  oarec  8038  oeeu  8079  domen  8370  xpsnen  8448  xpcomco  8454  xpassen  8458  inf2  8932  zfinf  8948  axinf2  8949  zfinf2  8951  rankuni  9138  scott0  9161  cp  9166  ween  9307  aceq1  9389  aceq0  9390  aceq2  9391  dfac5lem1  9395  dfac5lem2  9396  dfac5lem3  9397  kmlem3  9424  kmlem14  9435  kmlem15  9436  kmlem16  9437  cflem  9514  cf0  9519  cfval2  9528  cfss  9533  cfslb  9534  fin23lem32  9612  axdc2lem  9716  zfac  9728  ac9  9751  ac9s  9761  axpowndlem3  9867  zfcndrep  9882  zfcndun  9883  zfcndpow  9884  zfcndinf  9886  zfcndac  9887  axgroth5  10092  axgroth2  10093  axgroth6  10096  axgroth3  10099  axgroth4  10100  grothprim  10102  grothtsk  10103  genpass  10277  ltexprlem1  10304  ltexprlem4  10307  supaddc  11456  supadd  11457  supmul1  11458  supmullem2  11460  2rexuz  12149  nnwos  12164  hashgt23el  13633  hashfun  13646  wwlktovfo  14156  xpcogend  14168  cbvsum  14885  cbvprod  15102  iprodmul  15190  maxprmfct  15882  4sqlem12  16121  vdwmc  16143  cshwrepswhash1  16265  imasleval  16643  isacs2  16753  cicsym  16903  gsumval3eu  18745  lidlnz  19690  isbasis2g  21240  tgval2  21248  ntreq0  21369  lmff  21593  cmpfi  21700  is1stc2  21734  1stcelcls  21753  unisngl  21819  isfbas2  22127  elfg  22163  alexsubALTlem3  22341  ustfilxp  22504  metrest  22817  metuel2  22858  restmetu  22863  dchrvmasumlema  25758  istrkg2ld  25928  istrkg3ld  25929  1loopgrvd2  26968  wwlksnextsurj  27365  isgrpo  27965  nmo  29946  reuxfrdf  29947  rexunirn  29948  dmrab  29952  disjorf  30019  fcoinvbr  30048  mpomptxf  30115  cnvoprabOLD  30144  fpwrelmapffslem  30156  ordtconnlem1  30784  ddemeas  31112  omssubaddlem  31174  omssubadd  31175  eulerpartlemgvv  31251  bnj89  31608  bnj133  31614  bnj1019  31668  bnj1101  31673  bnj1109  31675  bnj1143  31679  bnj1198  31684  bnj1304  31708  bnj605  31795  bnj607  31804  bnj600  31807  bnj865  31811  bnj916  31821  bnj983  31839  bnj985  31841  bnj996  31843  bnj1033  31855  bnj1083  31864  bnj1090  31865  bnj1093  31866  bnj1110  31868  bnj1128  31876  bnj1145  31879  bnj1171  31886  bnj1172  31887  bnj1174  31889  bnj1176  31891  bnj1186  31893  bnj1189  31895  bnj1253  31903  bnj1279  31904  bnj1371  31915  bnj1374  31917  bnj1312  31944  exdifsn  31959  lfuhgr3  31978  loop1cycl  31992  satfvsucsuc  32220  satf0op  32232  axextprim  32535  axrepprim  32536  axunprim  32537  axpowprim  32538  axregprim  32539  axinfprim  32540  axacprim  32541  dftr6  32594  coep  32595  coepr  32596  dffr5  32597  dfpo2  32599  cnvco1  32603  cnvco2  32604  eldm3  32605  fundmpss  32617  dfdm5  32624  dfrn5  32625  elima4  32627  domep  32646  axextdfeq  32651  19.12b  32655  axextndbi  32658  brtxp  32950  brpprod  32955  brsset  32959  dfon3  32962  brtxpsd  32964  elfix  32973  dffix2  32975  sscoid  32983  dffun10  32984  elfuns  32985  elsingles  32988  snelsingles  32992  dfiota3  32993  brimg  33007  brapply  33008  brcup  33009  brcap  33010  brsuccf  33011  funpartlem  33012  brrestrict  33019  dfrecs2  33020  dfrdg4  33021  neifg  33328  bj-equsexval  33592  bj-eeanvw  33646  bj-clabel  33699  bj-denotes  33759  bj-rexvw  33768  bj-csbsnlem  33791  bj-snsetex  33880  bj-elsngl  33885  bj-snglc  33886  bj-nul  33947  bj-restpw  33982  bj-restuni  33987  bj-dfmpoa  34008  mptsnunlem  34150  topdifinffinlem  34159  difunieq  34186  wl-dfclab  34359  wl-dfrmosb  34384  wl-dfrmov  34385  poimirlem26  34449  ismblfin  34464  itg2addnclem3  34476  itg2addnc  34477  ismgmOLD  34660  sbcexfi  34927  sbccom2lem  34934  eldmres  35062  ecinn0  35139  ineleq  35140  moantr  35148  rnxrn  35177  rnxrnres  35178  dfcoss2  35192  dfcoss3  35193  1cossres  35205  cocossss  35212  rncossdmcoss  35226  eldmcoss2  35230  coss0  35250  cossid  35251  dfssr2  35270  eldmqs1cossres  35424  prtlem16  35536  prter2  35548  islshpat  35684  islpln5  36202  islvol5  36246  pmapglb  36437  polval2N  36573  cdlemftr3  37232  dibelval3  37814  dicelval3  37847  dihglb2  38009  sn-axrep5v  38638  prjspeclsp  38759  diophrex  38857  rp-isfinite6  39369  snen1g  39375  relintab  39428  imaiun1  39481  coiun1  39482  clsk3nimkb  39875  expandexn  40122  ismnuprim  40127  rr-groth  40132  19.36vv  40253  19.37vv  40255  pm11.58  40260  pm11.6  40262  pm13.192  40280  2sbc5g  40286  iotasbc2  40290  onfrALTlem5  40415  onfrALTlem1  40421  ax6e2nd  40431  2sb5nd  40433  en3lplem2VD  40717  onfrALTlem5VD  40758  relopabVD  40774  ax6e2ndVD  40781  2sb5ndVD  40783  ax6e2ndALT  40803  2sb5ndALT  40805  rfcnnnub  40832  inn0f  40874  stoweidlem34  41861  stoweidlem35  41862  stoweidlem60  41887  smfpimcc  42624  ichexmpl1  43113  sprid  43118  opeliun2xp  43859  eliunxp2  43860  setrec1lem3  44272  elpglem3  44295  eximp-surprise  44365