Theorem exbii 1851

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

Syntax hints:   ↔ wb 205  ∃wex 1782

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

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  2exbii  1852  3exbii  1853  exanali  1863  exancom  1865  19.43  1886  19.41vv  1955  19.41vvv  1956  19.41vvvv  1957  exdistr  1959  exdistr2  1963  3exdistr  1965  19.12vvv  1993  excom13  2165  exrot4  2167  2sb5  2272  dfsb7  2276  eeor  2330  eeorOLD  2331  19.12vv  2344  eean  2345  eeeanv  2347  ee4anv  2348  2sb8ef  2353  equsexALT  2419  2sb5rf  2472  2sb8e  2530  mo4  2561  eu6lem  2568  eubii  2580  sb8eulem  2593  cbvmovw  2597  cbvmow  2598  eu1  2607  sbmo  2611  2moswapv  2626  2moswap  2641  euae  2656  issetlem  2814  clabel  2882  sbabel  2939  sbabelOLD  2940  nabbib  3046  rextru  3078  rexbii2  3091  r2exlem  3144  r19.41v  3189  r19.41  3261  rexcom4  3286  rexcomOLD  3289  2ex2rexrot  3296  rexv  3500  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  ceqsex2  3530  ceqsex2v  3531  ceqsex3v  3532  gencbvex  3536  spc3egv  3594  spc3gv  3595  ceqsrexv  3644  rexabOLD  3692  rexrab2  3697  euxfrw  3718  euxfr  3720  euind  3721  reu6  3723  reu3  3724  2reuswap  3743  2reuswap2  3744  reuind  3750  2reu5lem3  3754  2reu5  3755  2rmoswap  3758  sbcimdv  3852  sbcg  3857  sbccomlem  3865  rmo2  3882  rmoanim  3889  rmoanimALT  3890  rexun  4191  reupick3  4320  euelss  4322  ndisj  4368  abn0OLD  4382  pssnel  4471  rexsns  4674  exsnrex  4685  snprc  4722  euabsn2  4730  reusn  4732  eusn  4735  elpreqpr  4868  elunirab  4925  uniprg  4926  uniprOLD  4928  uniun  4935  uniin  4936  uni0b  4938  uniintsn  4992  iuncom4  5006  dfiun2g  5034  dfiun2gOLD  5035  iunn0  5071  iunxiun  5101  disjor  5129  cbvopab2  5226  cbvopab2v  5230  unopab  5231  axrep1  5287  axrep4  5291  axrep5  5292  axrep6  5293  zfrep4  5297  axsepgfromrep  5298  axnulALT  5305  0ex  5308  vnex  5315  inex1  5318  inuni  5344  axpweq  5349  zfpow  5365  axpow2  5366  axpow3  5367  vpwex  5376  zfpair  5420  zfpair2  5429  el  5438  eqvinop  5488  copsexgw  5491  copsexg  5492  opabn0  5554  iunopab  5560  iunopabOLD  5561  dfid2  5577  dfid3  5578  opeliunxp  5744  xpiundi  5747  xpiundir  5748  elvvv  5752  csbxp  5776  eliunxp  5838  exopxfr  5844  relop  5851  opelco2g  5868  cnvco  5886  cnvuni  5887  dfdm3  5888  dfrn2  5889  dfrn3  5890  elrng  5892  dfdm4  5896  csbdm  5898  eldm2g  5900  dmun  5911  dmin  5912  dmiun  5914  dmuni  5915  dmopab  5916  dmi  5922  dmep  5924  rnep  5927  rnopab  5954  dmcosseq  5973  dmres  6004  elsnres  6022  dfima2  6062  elima3  6067  imadmrn  6070  imai  6074  args  6092  rniun  6148  xpdifid  6168  ssrnres  6178  dmsnn0  6207  dmsnopg  6213  cnvresima  6230  mptpreima  6238  dfco2  6245  coundi  6247  coundir  6248  resco  6250  imaco  6251  rnco  6252  coiun  6256  coi1  6262  coass  6265  xpco  6289  elsnxp  6291  dfpo2  6296  dffun2OLDOLD  6556  dffun5  6561  imadif  6633  funimaexgOLD  6636  brprcneu  6882  brprcneuALT  6883  dffv2  6987  fndmin  7047  fvn0ssdmfun  7077  abrexco  7243  imaiun  7244  isomin  7334  imaeqsexv  7360  dfoprab2  7467  cbvoprab2  7497  zfun  7726  uniex2  7728  uniuni  7749  elxp4  7913  elxp5  7914  fiun  7929  f1iun  7930  f11o  7933  fvresex  7946  opabex3d  7952  opabex3rd  7953  opabex3  7954  abexssex  7957  abexex  7958  oprabrexex2  7965  releldm2  8029  dfopab2  8038  dfoprab3s  8039  fsplit  8103  frxp  8112  suppvalbr  8150  cnvimadfsn  8157  brtpos2  8217  dfwrecsOLD  8298  wfrfunOLD  8319  dfrecs3  8372  dfrecs3OLD  8373  oarec  8562  oeeu  8603  domen  8957  xpsnen  9055  xpcomco  9062  xpassen  9066  dif1enOLD  9162  inf2  9618  zfinf  9634  axinf2  9635  zfinf2  9637  brttrcl2  9709  ttrcltr  9711  ttrclresv  9712  ttrclselem2  9721  rankuni  9858  scott0  9881  cp  9886  ween  10030  aceq1  10112  aceq0  10113  aceq2  10114  dfac5lem1  10118  dfac5lem2  10119  dfac5lem3  10120  kmlem3  10147  kmlem14  10158  kmlem15  10159  kmlem16  10160  cflem  10241  cf0  10246  cfval2  10255  cfss  10260  cfslb  10261  fin23lem32  10339  axdc2lem  10443  zfac  10455  ac9  10478  ac9s  10488  axpowndlem3  10594  zfcndrep  10609  zfcndun  10610  zfcndpow  10611  zfcndinf  10613  zfcndac  10614  axgroth5  10819  axgroth2  10820  axgroth6  10823  axgroth3  10826  axgroth4  10827  grothprim  10829  grothtsk  10830  genpass  11004  ltexprlem1  11031  ltexprlem4  11034  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  2rexuz  12884  nnwos  12899  hashgt23el  14384  hashfun  14397  wwlktovfo  14909  xpcogend  14921  cbvsum  15641  cbvprod  15859  iprodmul  15947  maxprmfct  16646  4sqlem12  16889  vdwmc  16911  cshwrepswhash1  17036  imasleval  17487  isacs2  17597  cicsym  17751  gsumval3eu  19772  lidlnz  20853  isbasis2g  22451  tgval2  22459  ntreq0  22581  lmff  22805  cmpfi  22912  is1stc2  22946  1stcelcls  22965  unisngl  23031  isfbas2  23339  elfg  23375  alexsubALTlem3  23553  ustfilxp  23717  metrest  24033  metuel2  24074  restmetu  24079  dchrvmasumlema  27003  elold  27365  lrrecfr  27429  sleadd1  27475  addsuniflem  27487  addsasslem1  27489  addsasslem2  27490  mulsuniflem  27607  addsdilem1  27609  addsdilem2  27610  mulsasslem1  27621  mulsasslem2  27622  istrkg2ld  27742  istrkg3ld  27743  1loopgrvd2  28791  wwlksnextsurj  29185  isgrpo  29781  nmo  31761  reuxfrdf  31762  rexunirn  31763  dmrab  31768  disjorf  31841  fcoinvbr  31867  mpomptxf  31936  cnvoprabOLD  31976  fpwrelmapffslem  31988  ordtconnlem1  32935  ddemeas  33265  omssubaddlem  33329  omssubadd  33330  eulerpartlemgvv  33406  bnj89  33763  bnj133  33769  bnj1019  33821  bnj1101  33826  bnj1109  33828  bnj1143  33832  bnj1198  33837  bnj1304  33861  bnj605  33949  bnj607  33958  bnj600  33961  bnj865  33965  bnj916  33975  bnj983  33993  bnj985v  33995  bnj985  33996  bnj996  33998  bnj1033  34011  bnj1083  34020  bnj1090  34021  bnj1093  34022  bnj1110  34024  bnj1128  34032  bnj1145  34035  bnj1171  34042  bnj1172  34043  bnj1174  34045  bnj1176  34047  bnj1186  34049  bnj1189  34051  bnj1253  34059  bnj1279  34060  bnj1371  34071  bnj1374  34073  bnj1312  34100  exdifsn  34115  fineqvrep  34126  fineqvpow  34127  lfuhgr3  34141  loop1cycl  34159  satfvsucsuc  34387  satf0op  34399  axextprim  34701  axrepprim  34702  axunprim  34703  axpowprim  34704  axregprim  34705  axinfprim  34706  axacprim  34707  dftr6  34752  coep  34753  coepr  34754  dffr5  34755  cnvco1  34760  cnvco2  34761  eldm3  34762  fundmpss  34769  dfdm5  34775  dfrn5  34776  elima4  34778  axextdfeq  34800  19.12b  34804  axextndbi  34807  brtxp  34883  brpprod  34888  brsset  34892  dfon3  34895  brtxpsd  34897  elfix  34906  dffix2  34908  sscoid  34916  dffun10  34917  elfuns  34918  elsingles  34921  snelsingles  34925  dfiota3  34926  brimg  34940  brapply  34941  brcup  34942  brcap  34943  brsuccf  34944  funpartlem  34945  brrestrict  34952  dfrecs2  34953  dfrdg4  34954  neifg  35304  bj-equsexval  35585  bj-eeanvw  35639  bj-substw  35648  eliminable-abelv  35796  eliminable-abelab  35797  bj-denoteslem  35798  bj-rexvw  35808  bj-csbsnlem  35831  bj-gabima  35868  bj-snsetex  35892  bj-elsngl  35897  bj-snglc  35898  bj-abex  35959  bj-clex  35960  bj-clel3gALT  35977  bj-nul  35985  bj-dfid2ALT  35994  bj-restpw  36021  bj-restuni  36026  bj-dfmpoa  36047  bj-opabco  36117  bj-xpcossxp  36118  bj-imdirco  36119  mptsnunlem  36267  topdifinffinlem  36276  difunieq  36303  wl-dfclab  36506  poimirlem26  36562  ismblfin  36577  itg2addnclem3  36589  itg2addnc  36590  ismgmOLD  36766  sbcexfi  37033  sbccom2lem  37040  eldmres  37186  ecinn0  37270  ineleq  37271  moantr  37281  rnxrn  37316  rnxrnres  37317  dfcoss2  37331  dfcoss3  37332  cosscnv  37334  coss1cnvres  37335  coss2cnvepres  37336  1cossres  37347  cocossss  37354  rncossdmcoss  37373  eldmcoss2  37377  coss0  37397  cossid  37398  dfssr2  37417  eldmqs1cossres  37577  prtlem16  37787  prter2  37799  islshpat  37935  islpln5  38454  islvol5  38498  pmapglb  38689  polval2N  38825  cdlemftr3  39484  dibelval3  40066  dicelval3  40099  dihglb2  40261  sn-axrep5v  41081  prjspeclsp  41402  diophrex  41561  onsupmaxb  42036  nnoeomeqom  42110  tfsconcatlem  42134  tfsconcat0i  42143  rp-isfinite6  42317  snen1g  42323  relintab  42382  imaiun1  42450  coiun1  42451  clsk3nimkb  42839  expandexn  43096  ismnuprim  43101  rr-groth  43106  ismnushort  43108  rr-grothshortbi  43110  19.36vv  43190  19.37vv  43192  pm11.58  43197  pm11.6  43199  pm13.192  43217  2sbc5g  43223  iotasbc2  43227  onfrALTlem5  43351  onfrALTlem1  43357  ax6e2nd  43367  2sb5nd  43369  en3lplem2VD  43653  onfrALTlem5VD  43694  relopabVD  43710  ax6e2ndVD  43717  2sb5ndVD  43719  ax6e2ndALT  43739  2sb5ndALT  43741  rfcnnnub  43768  inn0f  43808  stoweidlem34  44798  stoweidlem35  44799  stoweidlem60  44824  smfpimcc  45572  ichexmpl1  46185  sprid  46190  opeliun2xp  47056  eliunxp2  47057  mosssn2  47549  setrec1lem3  47782  elpglem3  47806  eximp-surprise  47879