Theorem exbii 1844

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

Syntax hints:   ↔ wb 206  ∃wex 1775

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

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

This theorem is referenced by:  2exbii  1845  3exbii  1846  exanali  1856  exancom  1858  19.43  1879  19.41vv  1947  19.41vvv  1948  19.41vvvv  1949  exdistr  1951  exdistr2  1955  3exdistr  1957  19.12vvv  1985  excom13  2161  exrot4  2163  2sb5  2275  dfsb7  2277  eeor  2333  eeorOLD  2334  19.12vv  2347  eean  2348  eeeanv  2350  ee4anv  2351  2sb8ef  2356  equsexALT  2421  2sb5rf  2474  2sb8e  2532  mo4  2563  eu6lem  2570  eubii  2582  sb8eulem  2595  cbvmovw  2599  cbvmow  2600  eu1  2607  sbmo  2611  2moswapv  2626  2moswap  2641  euae  2657  issettru  2816  issetlem  2818  clabel  2885  sbabel  2935  sbabelOLD  2936  nabbib  3042  rextru  3074  rexbii2  3087  r2exlem  3140  r19.41v  3186  r3ex  3195  r19.41  3260  rexcom4  3285  rexcomOLD  3288  2ex2rexrot  3295  rexv  3506  cgsex4gOLD  3526  ceqsex2  3534  ceqsex2v  3535  ceqsex3v  3536  gencbvex  3540  spc3egv  3602  spc3gv  3603  ceqsrexv  3654  rexabOLD  3703  rexrab2  3708  euxfrw  3729  euxfr  3731  euind  3732  reu6  3734  reu3  3735  2reuswap  3754  2reuswap2  3755  reuind  3761  2reu5lem3  3765  2reu5  3766  2rmoswap  3769  sbcimdv  3864  sbcg  3869  sbccomlemOLD  3878  rmo2  3895  rmoanim  3902  rmoanimALT  3903  rexun  4205  reupick3  4335  euelss  4337  ndisj  4375  inn0f  4376  pssnel  4476  rexsns  4675  exsnrex  4684  snprc  4721  euabsn2  4729  reusn  4731  eusn  4734  elpreqpr  4871  elunirab  4926  uniprg  4927  uniun  4934  uniin  4935  uni0b  4937  uniintsn  4989  iuncom4  5004  dfiun2g  5034  dfiun2gOLD  5035  iunn0  5071  iunxiun  5101  disjor  5129  cbvopab2  5224  cbvopab2v  5228  unopab  5229  axrep1  5285  axrep4v  5289  axrep4  5290  axrep4OLD  5291  axrep5  5292  axrep6  5293  axrep6OLD  5294  zfrep4  5298  axsepgfromrep  5299  axnulALT  5309  0ex  5312  vnex  5319  inex1  5322  inuni  5355  axpweq  5356  zfpow  5371  axpow2  5372  axpow3  5373  vpwex  5382  zfpair  5426  zfpair2  5438  el  5447  eqvinop  5497  copsexgw  5500  copsexg  5501  opabn0  5562  iunopab  5568  iunopabOLD  5569  dfid2  5584  dfid3  5585  opeliunxp  5755  xpiundi  5758  xpiundir  5759  elvvv  5763  csbxp  5787  eliunxp  5850  exopxfr  5856  relop  5863  opelco2g  5880  cnvco  5898  cnvuni  5899  dfdm3  5900  dfrn2  5901  dfrn3  5902  elrng  5904  dfdm4  5908  csbdm  5910  eldm2g  5912  dmun  5923  dmin  5924  dmiun  5926  dmuni  5927  dmopab  5928  dmi  5934  dmep  5936  rnep  5939  dmxp  5941  rnopab  5967  dmcosseq  5989  dmcosseqOLD  5990  dmres  6031  elsnres  6040  dfima2  6081  elima3  6086  imadmrn  6089  imai  6093  args  6112  rniun  6169  xpdifid  6189  ssrnres  6199  dmsnn0  6228  dmsnopg  6234  cnvresima  6251  mptpreima  6259  dfco2  6266  coundi  6268  coundir  6269  resco  6271  imaco  6272  rnco  6273  coiun  6277  coi1  6283  coass  6286  xpco  6310  elsnxp  6312  dfpo2  6317  dffun2OLDOLD  6574  dffun5  6579  imadif  6651  funimaexgOLD  6654  brprcneu  6896  brprcneuALT  6897  dffv2  7003  fndmin  7064  fvn0ssdmfun  7093  abrexco  7263  imaiun  7264  isomin  7356  imaeqsexvOLD  7382  dfoprab2  7490  cbvoprab2  7520  zfun  7754  uniex2  7756  uniuni  7780  elxp4  7944  elxp5  7945  fiun  7965  f1iun  7966  f11o  7969  fvresex  7982  opabex3d  7988  opabex3rd  7989  opabex3  7990  abexssex  7993  abexex  7994  oprabrexex2  8001  releldm2  8066  dfopab2  8075  dfoprab3s  8076  fsplit  8140  frxp  8149  suppvalbr  8187  cnvimadfsn  8195  brtpos2  8255  dfwrecsOLD  8336  wfrfunOLD  8357  dfrecs3  8410  dfrecs3OLD  8411  oarec  8598  oeeu  8639  domen  9000  xpsnen  9093  xpcomco  9100  xpassen  9104  dif1enOLD  9200  inf2  9660  zfinf  9676  axinf2  9677  zfinf2  9679  brttrcl2  9751  ttrcltr  9753  ttrclresv  9754  ttrclselem2  9763  rankuni  9900  scott0  9923  cp  9928  ween  10072  aceq1  10154  aceq0  10155  aceq2  10156  dfac5lem1  10160  dfac5lem2  10161  dfac5lem3  10162  kmlem3  10190  kmlem14  10201  kmlem15  10202  kmlem16  10203  cflem  10282  cflemOLD  10283  cf0  10288  cfval2  10297  cfss  10302  cfslb  10303  fin23lem32  10381  axdc2lem  10485  zfac  10497  ac9  10520  ac9s  10530  axpowndlem3  10636  zfcndrep  10651  zfcndun  10652  zfcndpow  10653  zfcndinf  10655  zfcndac  10656  axgroth5  10861  axgroth2  10862  axgroth6  10865  axgroth3  10868  axgroth4  10869  grothprim  10871  grothtsk  10872  genpass  11046  ltexprlem1  11073  ltexprlem4  11076  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  2rexuz  12939  nnwos  12954  hashgt23el  14459  hashfun  14472  wwlktovfo  14993  xpcogend  15009  cbvsum  15727  cbvsumv  15728  cbvprod  15945  cbvprodv  15946  prodeq1i  15948  iprodmul  16035  maxprmfct  16742  4sqlem12  16989  vdwmc  17011  cshwrepswhash1  17136  imasleval  17587  isacs2  17697  cicsym  17851  gsumval3eu  19936  lidlnz  21269  isbasis2g  22970  tgval2  22978  ntreq0  23100  lmff  23324  cmpfi  23431  is1stc2  23465  1stcelcls  23484  unisngl  23550  isfbas2  23858  elfg  23894  alexsubALTlem3  24072  ustfilxp  24236  metrest  24552  metuel2  24593  restmetu  24598  dchrvmasumlema  27558  elold  27922  lrrecfr  27990  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  mulsuniflem  28189  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  renegscl  28444  readdscl  28445  remulscl  28448  istrkg2ld  28482  istrkg3ld  28483  1loopgrvd2  29535  wwlksnextsurj  29929  isgrpo  30525  nmo  32517  reuxfrdf  32518  rexunirn  32519  dmrab  32524  disjorf  32598  fcoinvbr  32624  mpomptxf  32693  cnvoprabOLD  32737  fpwrelmapffslem  32749  1arithidom  33544  ordtconnlem1  33884  ddemeas  34216  omssubaddlem  34280  omssubadd  34281  eulerpartlemgvv  34357  bnj89  34713  bnj133  34719  bnj1019  34771  bnj1101  34776  bnj1109  34778  bnj1143  34782  bnj1198  34787  bnj1304  34811  bnj605  34899  bnj607  34908  bnj600  34911  bnj865  34915  bnj916  34925  bnj983  34943  bnj985v  34945  bnj985  34946  bnj996  34948  bnj1033  34961  bnj1083  34970  bnj1090  34971  bnj1093  34972  bnj1110  34974  bnj1128  34982  bnj1145  34985  bnj1171  34992  bnj1172  34993  bnj1174  34995  bnj1176  34997  bnj1186  34999  bnj1189  35001  bnj1253  35009  bnj1279  35010  bnj1371  35021  bnj1374  35023  bnj1312  35050  exdifsn  35071  fineqvrep  35087  fineqvpow  35088  lfuhgr3  35103  loop1cycl  35121  satfvsucsuc  35349  satf0op  35361  axextprim  35680  axrepprim  35681  axunprim  35682  axpowprim  35683  axregprim  35684  axinfprim  35685  axacprim  35686  dftr6  35730  coep  35731  coepr  35732  dffr5  35733  cnvco1  35738  cnvco2  35739  eldm3  35740  fundmpss  35747  dfdm5  35753  dfrn5  35754  elima4  35756  axextdfeq  35778  19.12b  35782  axextndbi  35785  brtxp  35861  brpprod  35866  brsset  35870  dfon3  35873  brtxpsd  35875  elfix  35884  dffix2  35886  sscoid  35894  dffun10  35895  elfuns  35896  elsingles  35899  snelsingles  35903  dfiota3  35904  brimg  35918  brapply  35919  brcup  35920  brcap  35921  brsuccf  35922  funpartlem  35923  brrestrict  35930  dfrecs2  35931  dfrdg4  35932  sumeq2si  36183  prodeq2si  36185  cbvoprab2vw  36220  cbvoprab23vw  36222  cbvprodvw2  36229  neifg  36353  bj-equsexval  36642  bj-eeanvw  36695  bj-substw  36704  eliminable-abelv  36851  eliminable-abelab  36852  bj-denoteslem  36853  bj-rexvw  36862  bj-csbsnlem  36885  bj-gabima  36922  bj-snsetex  36945  bj-elsngl  36950  bj-snglc  36951  bj-abex  37012  bj-clex  37013  bj-clel3gALT  37030  bj-nul  37038  bj-dfid2ALT  37047  bj-restpw  37074  bj-restuni  37079  bj-dfmpoa  37100  bj-opabco  37170  bj-xpcossxp  37171  bj-imdirco  37172  mptsnunlem  37320  topdifinffinlem  37329  difunieq  37356  wl-dfclab  37576  poimirlem26  37632  ismblfin  37647  itg2addnclem3  37659  itg2addnc  37660  ismgmOLD  37836  sbcexfi  38103  sbccom2lem  38110  eldmres  38251  ecinn0  38334  ineleq  38335  moantr  38345  rnxrn  38379  rnxrnres  38380  dfcoss2  38394  dfcoss3  38395  cosscnv  38397  coss1cnvres  38398  coss2cnvepres  38399  1cossres  38410  cocossss  38417  rncossdmcoss  38436  eldmcoss2  38440  coss0  38460  cossid  38461  dfssr2  38480  eldmqs1cossres  38640  prtlem16  38850  prter2  38862  islshpat  38998  islpln5  39517  islvol5  39561  pmapglb  39752  polval2N  39888  cdlemftr3  40547  dibelval3  41129  dicelval3  41162  dihglb2  41324  sn-axrep5v  42233  prjspeclsp  42598  euabsn2w  42665  diophrex  42762  onsupmaxb  43227  nnoeomeqom  43301  tfsconcatlem  43325  tfsconcat0i  43334  rp-isfinite6  43507  snen1g  43513  relintab  43572  imaiun1  43640  coiun1  43641  clsk3nimkb  44029  expandexn  44284  ismnuprim  44289  rr-groth  44294  ismnushort  44296  rr-grothshortbi  44298  19.36vv  44378  19.37vv  44380  pm11.58  44385  pm11.6  44387  pm13.192  44405  2sbc5g  44411  iotasbc2  44415  onfrALTlem5  44539  onfrALTlem1  44545  ax6e2nd  44555  2sb5nd  44557  en3lplem2VD  44841  onfrALTlem5VD  44882  relopabVD  44898  ax6e2ndVD  44905  2sb5ndVD  44907  ax6e2ndALT  44927  2sb5ndALT  44929  rfcnnnub  44973  stoweidlem34  45989  stoweidlem35  45990  stoweidlem60  46015  smfpimcc  46763  ichexmpl1  47393  sprid  47398  dfgric2  47821  usgrgrtrirex  47852  grlimgrtri  47898  opeliun2xp  48177  eliunxp2  48178  mosssn2  48664  setrec1lem3  48919  elpglem3  48943  eximp-surprise  49014