Theorem exbii 1764

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

Syntax hints:   ↔ wb 195  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  2exbii  1765  3exbii  1766  nfbii  1770  exanali  1773  exancom  1774  19.43  1799  sbequ8  1872  19.12vvv  1894  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  exdistr  1906  19.42vvv  1908  exdistr2  1909  3exdistr  1910  equsexvw  1919  excom13  2031  exrot4  2033  equsexv  2095  eeor  2157  19.12vv  2168  eean  2169  eeeanv  2171  ee4anv  2172  equsexALT  2282  2sb5  2431  2sb5rf  2439  2sb8e  2455  sb8eu  2491  eu1  2498  sbmo  2503  2moswap  2535  exists1  2549  clabel  2736  sbabel  2779  nabbi  2884  rexbii2  3021  r2exlem  3041  r19.41v  3070  r19.41  3071  isset  3180  rexv  3193  ceqsex2  3217  ceqsex3v  3219  gencbvex  3223  vtocl2  3234  vtocl3  3235  spc3gv  3271  ceqsrexv  3306  rexab  3336  rexrab2  3341  euxfr  3359  euind  3360  reu6  3362  reu3  3363  2reuswap  3377  reuind  3378  2reu5lem3  3382  2reu5  3383  sbccomlem  3475  rmo2  3492  rexun  3755  reupick3  3871  euelss  3873  abn0  3908  pssnel  3991  rexsns  4164  exsnrex  4168  snprc  4197  euabsn2  4204  reusn  4206  eusn  4209  elpreqpr  4334  elunirab  4384  unipr  4385  uniun  4392  uniin  4393  uni0b  4399  uniintsn  4449  iuncom4  4464  dfiun2g  4488  iunn0  4516  iunxiun  4544  disjor  4567  cbvopab2  4656  cbvopab2v  4659  unopab  4660  axrep1  4700  axrep4  4703  axrep5  4704  zfrep4  4707  axsep  4708  zfnuleu  4714  axnulALT  4715  0ex  4718  vprc  4724  inex1  4727  inuni  4753  axpweq  4768  zfpow  4770  axpow2  4771  axpow3  4772  pwex  4774  zfpair  4831  zfpair2  4834  eqvinop  4881  copsexg  4882  opabn0  4931  iunopab  4936  dfid3  4954  elxp2OLD  5057  opeliunxp  5093  xpiundi  5096  xpiundir  5097  elvvv  5101  csbxp  5123  eliunxp  5181  exopxfr  5187  relop  5194  opelco2g  5211  cnvco  5230  cnvuni  5231  dfdm3  5232  dfrn2  5233  dfrn3  5234  elrng  5236  dfdm4  5238  csbdm  5240  eldm2g  5242  dmun  5253  dmin  5254  dmiun  5255  dmuni  5256  dmopab  5257  dmi  5261  elrn  5287  rnopab  5291  dmcosseq  5308  dmres  5339  elres  5355  elsnres  5356  dfima2  5387  elima3  5392  imadmrn  5395  imai  5397  args  5412  rniun  5462  xpdifid  5481  ssrnres  5491  dmsnn0  5518  dmsnopg  5524  cnvresima  5541  mptpreima  5545  dfco2  5551  coundi  5553  coundir  5554  resco  5556  imaco  5557  rnco  5558  coiun  5562  coi1  5568  coass  5571  xpco  5592  elsnxp  5594  elsnxpOLD  5595  dffun2  5814  dffun5  5817  imadif  5887  funimaexg  5889  brprcneu  6096  dffv2  6181  fndmin  6232  fvn0ssdmfun  6258  abrexco  6406  imaiun  6407  isomin  6487  dfoprab2  6599  cbvoprab2  6626  zfun  6848  uniex2  6850  uniuni  6865  elxp4  7003  elxp5  7004  fun11iun  7019  f11o  7021  fvresex  7032  opabex3d  7037  opabex3  7038  abexssex  7041  abexex  7042  oprabrexex2  7049  releldm2  7109  dfopab2  7113  dfoprab3s  7114  fsplit  7169  frxp  7174  suppvalbr  7186  cnvimadfsn  7191  brtpos2  7245  wfrfun  7312  dfrecs3  7356  oarec  7529  oeeu  7570  domen  7854  mapsnen  7920  xpsnen  7929  xpcomco  7935  xpassen  7939  inf2  8403  zfinf  8419  axinf2  8420  zfinf2  8422  rankuni  8609  scott0  8632  cp  8637  ween  8741  aceq1  8823  aceq0  8824  aceq2  8825  dfac5lem1  8829  dfac5lem2  8830  dfac5lem3  8831  kmlem3  8857  kmlem14  8868  kmlem15  8869  kmlem16  8870  cflem  8951  cf0  8956  cfval2  8965  cfss  8970  cfslb  8971  fin23lem32  9049  axdc2lem  9153  zfac  9165  ac9  9188  ac9s  9198  axpowndlem3  9300  zfcndrep  9315  zfcndun  9316  zfcndpow  9317  zfcndinf  9319  zfcndac  9320  axgroth5  9525  axgroth2  9526  grothpw  9527  axgroth6  9529  axgroth3  9532  axgroth4  9533  grothprim  9535  grothtsk  9536  genpass  9710  ltexprlem1  9737  ltexprlem4  9740  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  2rexuz  11616  nnwos  11631  hashfun  13084  wwlktovfo  13549  xpcogend  13561  cbvsum  14273  cbvprod  14484  iprodmul  14573  maxprmfct  15259  4sqlem12  15498  vdwmc  15520  cshwrepswhash1  15647  imasleval  16024  isacs2  16137  cicsym  16287  gsumval3eu  18128  lidlnz  19049  isbasis2g  20563  tgval2  20571  ntreq0  20691  lmff  20915  cmpfi  21021  is1stc2  21055  1stcelcls  21074  unisngl  21140  isfbas2  21449  elfg  21485  alexsubALTlem3  21663  ustfilxp  21826  metrest  22139  metuel2  22180  restmetu  22185  cmetss  22921  dchrvmasumlema  24989  istrkg2ld  25159  istrkg3ld  25160  usgraedg4  25916  3v3e3cycl2  26192  wlknwwlknsur  26240  wlkiswwlksur  26247  wwlkextsur  26259  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  frgrawopreglem2  26572  usg2spot2nb  26592  isgrpo  26735  nmo  28709  2reuswap2  28712  rexunirn  28715  iunxsngf  28758  disjorf  28774  fcoinvbr  28799  mpt2mptxf  28860  cnvoprab  28886  fpwrelmapffslem  28895  ordtconlem1  29298  ddemeas  29626  omssubaddlem  29688  omssubadd  29689  eulerpartlemgvv  29765  bnj89  30041  bnj133  30047  bnj1019  30104  bnj1101  30109  bnj1109  30111  bnj1143  30115  bnj1198  30120  bnj1304  30144  bnj605  30231  bnj607  30240  bnj600  30243  bnj865  30247  bnj916  30257  bnj983  30275  bnj985  30277  bnj996  30279  bnj1033  30291  bnj1083  30300  bnj1090  30301  bnj1093  30302  bnj1110  30304  bnj1128  30312  bnj1145  30315  bnj1171  30322  bnj1172  30323  bnj1174  30325  bnj1176  30327  bnj1186  30329  bnj1189  30331  bnj1253  30339  bnj1279  30340  bnj1371  30351  bnj1374  30353  bnj1312  30380  axextprim  30832  axrepprim  30833  axunprim  30834  axpowprim  30835  axregprim  30836  axinfprim  30837  axacprim  30838  dftr6  30893  coep  30894  coepr  30895  dffr5  30896  dfpo2  30898  cnvco1  30903  cnvco2  30904  eldm3  30905  fundmpss  30910  dfdm5  30921  dfrn5  30922  elima4  30924  domep  30942  axextdfeq  30947  19.12b  30951  axextndbi  30954  frrlem5c  31030  nofulllem5  31105  brtxp  31157  brpprod  31162  brsset  31166  dfon3  31169  brtxpsd  31171  elfix  31180  dffix2  31182  sscoid  31190  dffun10  31191  elfuns  31192  elsingles  31195  snelsingles  31199  dfiota3  31200  brimg  31214  brapply  31215  brcup  31216  brcap  31217  brsuccf  31218  funpartlem  31219  brrestrict  31226  dfrecs2  31227  dfrdg4  31228  neifg  31536  bj-equsexval  31827  bj-dfssb2  31829  bj-eeanvw  31891  bj-clabel  31971  bj-axrep1  31976  bj-axrep4  31979  bj-axrep5  31980  bj-axsep  31981  bj-zfpow  31983  bj-denotes  32052  bj-rexvwv  32060  bj-rexcom4  32063  bj-csbsnlem  32090  bj-snsetex  32144  bj-elsngl  32149  bj-snglc  32150  bj-nul  32209  bj-restpw  32226  bj-restuni  32231  bj-dfmpt2a  32252  mptsnunlem  32361  topdifinffinlem  32371  poimirlem26  32605  ismblfin  32620  itg2addnclem3  32633  itg2addnc  32634  ismgmOLD  32819  sbcexfi  33090  sbccom2lem  33099  prtlem16  33172  prter2  33184  islshpat  33322  islpln5  33839  islvol5  33883  pmapglb  34074  polval2N  34210  cdlemftr3  34871  dibelval3  35454  dicelval3  35487  dihglb2  35649  diophrex  36357  rp-isfinite6  36883  relintab  36908  imaiun1  36962  coiun1  36963  ndisj  37083  clsk3nimkb  37358  19.36vv  37604  19.37vv  37606  pm11.58  37612  pm11.6  37614  pm13.192  37633  2sbc5g  37639  iotasbc2  37643  onfrALTlem5  37778  onfrALTlem1  37784  ax6e2nd  37795  2sb5nd  37797  en3lplem2VD  38101  relopabVD  38159  ax6e2ndVD  38166  2sb5ndVD  38168  ax6e2ndALT  38188  2sb5ndALT  38190  rfcnnnub  38218  inn0f  38268  stoweidlem34  38927  stoweidlem35  38928  stoweidlem60  38953  rmoanim  39828  2rmoswap  39833  1loopgrvd2  40718  wlknwwlksnsur  41087  wlkwwlksur  41094  wwlksnextsur  41106  frgrwopreglem2  41482  fusgr2wsp2nb  41498  opeliun2xp  41904  eliunxp2  41905  setrec1lem3  42235  elpglem3  42255  eximp-surprise  42339