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 205  ∃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 206  df-ex 1782

This theorem is referenced by:  2exbii  1851  3exbii  1852  exanali  1862  exancom  1864  19.43  1885  19.41vv  1954  19.41vvv  1955  19.41vvvv  1956  exdistr  1958  exdistr2  1962  3exdistr  1964  19.12vvv  1992  excom13  2164  exrot4  2166  2sb5  2271  dfsb7  2275  eeor  2329  eeorOLD  2330  19.12vv  2343  eean  2344  eeeanv  2346  ee4anv  2347  2sb8ef  2352  equsexALT  2417  2sb5rf  2470  2sb8e  2528  mo4  2559  eu6lem  2566  eubii  2578  sb8eulem  2591  cbvmovw  2595  cbvmow  2596  eu1  2605  sbmo  2609  2moswapv  2624  2moswap  2639  euae  2654  issetlem  2812  clabel  2880  sbabel  2937  sbabelOLD  2938  nabbi  3044  rextru  3076  rexbii2  3089  r2exlem  3136  r19.41v  3181  r19.41  3244  rexcom4  3269  rexcomOLD  3272  2ex2rexrot  3279  rexv  3471  cgsex4g  3491  cgsex4gOLD  3492  ceqsex2  3499  ceqsex2v  3500  ceqsex3v  3501  gencbvex  3505  spc3egv  3563  spc3gv  3564  ceqsrexv  3608  rexabOLD  3656  rexrab2  3661  euxfrw  3682  euxfr  3684  euind  3685  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  reuind  3714  2reu5lem3  3718  2reu5  3719  2rmoswap  3722  sbcimdv  3816  sbcg  3821  sbccomlem  3829  rmo2  3846  rmoanim  3853  rmoanimALT  3854  rexun  4155  reupick3  4284  euelss  4286  ndisj  4332  abn0OLD  4346  pssnel  4435  rexsns  4635  exsnrex  4646  snprc  4683  euabsn2  4691  reusn  4693  eusn  4696  elpreqpr  4829  elunirab  4886  uniprg  4887  uniprOLD  4889  uniun  4896  uniin  4897  uni0b  4899  uniintsn  4953  iuncom4  4967  dfiun2g  4995  dfiun2gOLD  4996  iunn0  5032  iunxiun  5062  disjor  5090  cbvopab2  5187  cbvopab2v  5191  unopab  5192  axrep1  5248  axrep4  5252  axrep5  5253  axrep6  5254  zfrep4  5258  axsepgfromrep  5259  axnulALT  5266  0ex  5269  vnex  5276  inex1  5279  inuni  5305  axpweq  5310  zfpow  5326  axpow2  5327  axpow3  5328  vpwex  5337  zfpair  5381  zfpair2  5390  el  5399  eqvinop  5449  copsexgw  5452  copsexg  5453  opabn0  5515  iunopab  5521  iunopabOLD  5522  dfid2  5538  dfid3  5539  opeliunxp  5704  xpiundi  5707  xpiundir  5708  elvvv  5712  csbxp  5736  eliunxp  5798  exopxfr  5804  relop  5811  opelco2g  5828  cnvco  5846  cnvuni  5847  dfdm3  5848  dfrn2  5849  dfrn3  5850  elrng  5852  dfdm4  5856  csbdm  5858  eldm2g  5860  dmun  5871  dmin  5872  dmiun  5874  dmuni  5875  dmopab  5876  dmi  5882  dmep  5884  rnep  5887  rnopab  5914  dmcosseq  5933  dmres  5964  elsnres  5982  dfima2  6020  elima3  6025  imadmrn  6028  imai  6031  args  6049  rniun  6105  xpdifid  6125  ssrnres  6135  dmsnn0  6164  dmsnopg  6170  cnvresima  6187  mptpreima  6195  dfco2  6202  coundi  6204  coundir  6205  resco  6207  imaco  6208  rnco  6209  coiun  6213  coi1  6219  coass  6222  xpco  6246  elsnxp  6248  dfpo2  6253  dffun2OLDOLD  6513  dffun5  6518  imadif  6590  funimaexgOLD  6593  brprcneu  6837  brprcneuALT  6838  dffv2  6941  fndmin  7000  fvn0ssdmfun  7030  abrexco  7196  imaiun  7197  isomin  7287  imaeqsexv  7313  dfoprab2  7420  cbvoprab2  7450  zfun  7678  uniex2  7680  uniuni  7701  elxp4  7864  elxp5  7865  fiun  7880  f1iun  7881  f11o  7884  fvresex  7897  opabex3d  7903  opabex3rd  7904  opabex3  7905  abexssex  7908  abexex  7909  oprabrexex2  7916  releldm2  7980  dfopab2  7989  dfoprab3s  7990  fsplit  8054  frxp  8063  suppvalbr  8101  cnvimadfsn  8108  brtpos2  8168  dfwrecsOLD  8249  wfrfunOLD  8270  dfrecs3  8323  dfrecs3OLD  8324  oarec  8514  oeeu  8555  domen  8908  xpsnen  9006  xpcomco  9013  xpassen  9017  dif1enOLD  9113  inf2  9568  zfinf  9584  axinf2  9585  zfinf2  9587  brttrcl2  9659  ttrcltr  9661  ttrclresv  9662  ttrclselem2  9671  rankuni  9808  scott0  9831  cp  9836  ween  9980  aceq1  10062  aceq0  10063  aceq2  10064  dfac5lem1  10068  dfac5lem2  10069  dfac5lem3  10070  kmlem3  10097  kmlem14  10108  kmlem15  10109  kmlem16  10110  cflem  10191  cf0  10196  cfval2  10205  cfss  10210  cfslb  10211  fin23lem32  10289  axdc2lem  10393  zfac  10405  ac9  10428  ac9s  10438  axpowndlem3  10544  zfcndrep  10559  zfcndun  10560  zfcndpow  10561  zfcndinf  10563  zfcndac  10564  axgroth5  10769  axgroth2  10770  axgroth6  10773  axgroth3  10776  axgroth4  10777  grothprim  10779  grothtsk  10780  genpass  10954  ltexprlem1  10981  ltexprlem4  10984  supaddc  12131  supadd  12132  supmul1  12133  supmullem2  12135  2rexuz  12834  nnwos  12849  hashgt23el  14334  hashfun  14347  wwlktovfo  14859  xpcogend  14871  cbvsum  15591  cbvprod  15809  iprodmul  15897  maxprmfct  16596  4sqlem12  16839  vdwmc  16861  cshwrepswhash1  16986  imasleval  17437  isacs2  17547  cicsym  17701  gsumval3eu  19695  lidlnz  20757  isbasis2g  22335  tgval2  22343  ntreq0  22465  lmff  22689  cmpfi  22796  is1stc2  22830  1stcelcls  22849  unisngl  22915  isfbas2  23223  elfg  23259  alexsubALTlem3  23437  ustfilxp  23601  metrest  23917  metuel2  23958  restmetu  23963  dchrvmasumlema  26885  elold  27242  lrrecfr  27298  sleadd1  27341  addsunif  27353  addsasslem1  27354  addsasslem2  27355  istrkg2ld  27465  istrkg3ld  27466  1loopgrvd2  28514  wwlksnextsurj  28908  isgrpo  29502  nmo  31482  reuxfrdf  31483  rexunirn  31484  dmrab  31489  disjorf  31564  fcoinvbr  31593  mpomptxf  31664  cnvoprabOLD  31705  fpwrelmapffslem  31717  ordtconnlem1  32594  ddemeas  32924  omssubaddlem  32988  omssubadd  32989  eulerpartlemgvv  33065  bnj89  33422  bnj133  33428  bnj1019  33480  bnj1101  33485  bnj1109  33487  bnj1143  33491  bnj1198  33496  bnj1304  33520  bnj605  33608  bnj607  33617  bnj600  33620  bnj865  33624  bnj916  33634  bnj983  33652  bnj985v  33654  bnj985  33655  bnj996  33657  bnj1033  33670  bnj1083  33679  bnj1090  33680  bnj1093  33681  bnj1110  33683  bnj1128  33691  bnj1145  33694  bnj1171  33701  bnj1172  33702  bnj1174  33704  bnj1176  33706  bnj1186  33708  bnj1189  33710  bnj1253  33718  bnj1279  33719  bnj1371  33730  bnj1374  33732  bnj1312  33759  exdifsn  33774  fineqvrep  33785  fineqvpow  33786  lfuhgr3  33800  loop1cycl  33818  satfvsucsuc  34046  satf0op  34058  axextprim  34359  axrepprim  34360  axunprim  34361  axpowprim  34362  axregprim  34363  axinfprim  34364  axacprim  34365  dftr6  34410  coep  34411  coepr  34412  dffr5  34413  cnvco1  34418  cnvco2  34419  eldm3  34420  fundmpss  34427  dfdm5  34433  dfrn5  34434  elima4  34436  axextdfeq  34458  19.12b  34462  axextndbi  34465  brtxp  34541  brpprod  34546  brsset  34550  dfon3  34553  brtxpsd  34555  elfix  34564  dffix2  34566  sscoid  34574  dffun10  34575  elfuns  34576  elsingles  34579  snelsingles  34583  dfiota3  34584  brimg  34598  brapply  34599  brcup  34600  brcap  34601  brsuccf  34602  funpartlem  34603  brrestrict  34610  dfrecs2  34611  dfrdg4  34612  neifg  34919  bj-equsexval  35200  bj-eeanvw  35254  bj-substw  35263  eliminable-abelv  35411  eliminable-abelab  35412  bj-denoteslem  35413  bj-rexvw  35423  bj-csbsnlem  35446  bj-gabima  35483  bj-snsetex  35507  bj-elsngl  35512  bj-snglc  35513  bj-abex  35574  bj-clex  35575  bj-clel3gALT  35592  bj-nul  35600  bj-dfid2ALT  35609  bj-restpw  35636  bj-restuni  35641  bj-dfmpoa  35662  bj-opabco  35732  bj-xpcossxp  35733  bj-imdirco  35734  mptsnunlem  35882  topdifinffinlem  35891  difunieq  35918  wl-dfclab  36121  poimirlem26  36177  ismblfin  36192  itg2addnclem3  36204  itg2addnc  36205  ismgmOLD  36382  sbcexfi  36649  sbccom2lem  36656  eldmres  36803  ecinn0  36887  ineleq  36888  moantr  36898  rnxrn  36933  rnxrnres  36934  dfcoss2  36948  dfcoss3  36949  cosscnv  36951  coss1cnvres  36952  coss2cnvepres  36953  1cossres  36964  cocossss  36971  rncossdmcoss  36990  eldmcoss2  36994  coss0  37014  cossid  37015  dfssr2  37034  eldmqs1cossres  37194  prtlem16  37404  prter2  37416  islshpat  37552  islpln5  38071  islvol5  38115  pmapglb  38306  polval2N  38442  cdlemftr3  39101  dibelval3  39683  dicelval3  39716  dihglb2  39878  sn-axrep5v  40709  prjspeclsp  41008  diophrex  41156  onsupmaxb  41631  nnoeomeqom  41705  tfsconcatlem  41729  tfsconcat0i  41738  rp-isfinite6  41912  snen1g  41918  relintab  41977  imaiun1  42045  coiun1  42046  clsk3nimkb  42434  expandexn  42691  ismnuprim  42696  rr-groth  42701  ismnushort  42703  rr-grothshortbi  42705  19.36vv  42785  19.37vv  42787  pm11.58  42792  pm11.6  42794  pm13.192  42812  2sbc5g  42818  iotasbc2  42822  onfrALTlem5  42946  onfrALTlem1  42952  ax6e2nd  42962  2sb5nd  42964  en3lplem2VD  43248  onfrALTlem5VD  43289  relopabVD  43305  ax6e2ndVD  43312  2sb5ndVD  43314  ax6e2ndALT  43334  2sb5ndALT  43336  rfcnnnub  43363  inn0f  43403  stoweidlem34  44395  stoweidlem35  44396  stoweidlem60  44421  smfpimcc  45169  ichexmpl1  45781  sprid  45786  opeliun2xp  46528  eliunxp2  46529  mosssn2  47021  setrec1lem3  47254  elpglem3  47278  eximp-surprise  47351