Theorem exbii 1849

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

Syntax hints:   ↔ wb 206  ∃wex 1780

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

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

This theorem is referenced by:  2exbii  1850  3exbii  1851  exanali  1860  exancom  1862  19.43  1883  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistr  1955  exdistr2  1959  3exdistr  1961  19.12vvv  1995  excom13  2167  exrot4  2169  2sb5  2280  dfsb7  2281  eeor  2334  19.12vv  2347  eean  2348  eeeanv  2350  ee4anv  2351  ee4anvOLD  2352  2sb8ef  2356  equsexALT  2419  2sb5rf  2472  2sb8e  2530  mo4  2561  eu6lem  2568  eubii  2580  sb8eulem  2593  cbvmovw  2597  cbvmow  2598  eu1  2605  sbmo  2609  2moswapv  2624  2moswap  2639  euae  2655  issettru  2809  issetlem  2811  clabel  2877  sbabel  2927  nabbib  3031  rextru  3063  rexbii2  3075  r2exlem  3121  r19.41v  3162  r3ex  3171  r19.41  3236  rexcom4  3259  2ex2rexrot  3267  rexv  3464  cgsex4gOLD  3484  ceqsex2  3489  ceqsex2v  3490  ceqsex3v  3491  gencbvex  3495  spc3egv  3553  spc3gv  3554  ceqsrexv  3605  rexrab2  3654  euxfrw  3675  euxfr  3677  euind  3678  reu6  3680  reu3  3681  2reuswap  3700  2reuswap2  3701  reuind  3707  2reu5lem3  3711  2reu5  3712  2rmoswap  3715  sbcimdv  3805  sbcg  3809  sbccomlemOLD  3816  rmo2  3833  rmoanim  3840  rmoanimALT  3841  rexun  4145  reupick3  4279  euelss  4281  ndisj  4319  inn0f  4320  pssnel  4420  rexsns  4623  exsnrex  4632  snprc  4669  euabsn2  4677  reusn  4679  eusn  4682  elpreqpr  4818  elunirab  4873  uniprg  4874  uniun  4881  uniin  4882  uni0b  4884  uniintsn  4935  iuncom4  4950  dfiun2g  4980  iunn0  5017  iunxiun  5047  disjor  5075  cbvopab2  5169  cbvopab2v  5172  unopab  5173  axrep1  5220  axrep4v  5224  axrep4  5225  axrep4OLD  5226  axrep5  5227  axrep6  5228  axrep6OLD  5229  zfrep4  5233  axsepgfromrep  5234  axnulALT  5244  0ex  5247  vnex  5254  inex1  5257  inuni  5290  axpweq  5291  zfpow  5306  axpow2  5307  vpwex  5317  zfpair  5361  zfpair2  5373  el  5382  eqvinop  5430  copsexgw  5433  copsexg  5434  opabn0  5496  iunopab  5502  dfid2  5516  dfid3  5517  opeliunxp  5686  opeliun2xp  5687  xpiundi  5690  xpiundir  5691  elvvv  5695  csbxp  5720  eliunxp  5782  exopxfr  5788  relop  5795  opelco2g  5812  cnvco  5830  cnvuni  5831  dfdm3  5832  dfrn2  5833  dfrn3  5834  elrng  5836  dfdm4  5840  csbdm  5842  eldm2g  5844  dmun  5855  dmin  5856  dmiun  5858  dmuni  5859  dmopab  5860  dmi  5866  dmep  5868  rnep  5872  dmxp  5874  rnopab  5899  dmcosseq  5922  dmcosseqOLD  5923  dmcosseqOLDOLD  5924  dmres  5966  elsnres  5975  dfima2  6016  elima3  6021  imadmrn  6024  imai  6028  args  6046  rniun  6100  xpdifid  6121  ssrnres  6131  dmsnn0  6160  dmsnopg  6166  cnvresima  6183  mptpreima  6191  dfco2  6198  coundi  6200  coundir  6201  resco  6203  imaco  6204  rnco  6205  rncoOLD  6206  coiun  6210  coi1  6216  coass  6219  xpco  6242  elsnxp  6244  dfpo2  6249  dffun5  6501  imadif  6571  tz6.12-2  6815  brprcneu  6818  brprcneuALT  6819  dffv2  6923  fndmin  6984  fvn0ssdmfun  7013  abrexco  7184  imaiun  7185  isomin  7277  imaeqsexvOLD  7303  dfoprab2  7410  cbvoprab2  7440  zfun  7675  uniex2  7677  uniuni  7701  elxp4  7858  elxp5  7859  fiun  7881  f1iun  7882  f11o  7885  fvresex  7898  opabex3d  7903  opabex3rd  7904  opabex3  7905  abexssex  7908  abexex  7909  oprabrexex2  7916  releldm2  7981  dfopab2  7990  dfoprab3s  7991  fsplit  8053  frxp  8062  suppvalbr  8100  cnvimadfsn  8108  brtpos2  8168  dfrecs3  8298  oarec  8483  oeeu  8524  domen  8890  xpsnen  8980  xpcomco  8986  xpassen  8990  inf2  9519  zfinf  9535  axinf2  9536  zfinf2  9538  brttrcl2  9610  ttrcltr  9612  ttrclresv  9613  ttrclselem2  9622  rankuni  9762  scott0  9785  cp  9790  ween  9932  aceq1  10014  aceq0  10015  aceq2  10016  dfac5lem1  10020  dfac5lem2  10021  dfac5lem3  10022  kmlem3  10050  kmlem14  10061  kmlem15  10062  kmlem16  10063  cflem  10142  cflemOLD  10143  cf0  10148  cfval2  10157  cfss  10162  cfslb  10163  fin23lem32  10241  axdc2lem  10345  zfac  10357  ac9  10380  ac9s  10390  axpowndlem3  10496  zfcndrep  10511  zfcndun  10512  zfcndpow  10513  zfcndinf  10515  zfcndac  10516  axgroth5  10721  axgroth2  10722  axgroth6  10725  axgroth3  10728  axgroth4  10729  grothprim  10731  grothtsk  10732  genpass  10906  ltexprlem1  10933  ltexprlem4  10936  supaddc  12095  supadd  12096  supmul1  12097  supmullem2  12099  2rexuz  12804  nnwos  12819  hashgt23el  14337  hashfun  14350  wwlktovfo  14871  xpcogend  14887  cbvsum  15608  cbvsumv  15609  cbvprod  15826  cbvprodv  15827  prodeq1i  15829  iprodmul  15916  maxprmfct  16626  4sqlem12  16874  vdwmc  16896  cshwrepswhash1  17020  imasleval  17451  isacs2  17565  cicsym  17717  gsumval3eu  19822  lidlnz  21185  isbasis2g  22869  tgval2  22877  ntreq0  22998  lmff  23222  cmpfi  23329  is1stc2  23363  1stcelcls  23382  unisngl  23448  isfbas2  23756  elfg  23792  alexsubALTlem3  23970  ustfilxp  24134  metrest  24445  metuel2  24486  restmetu  24491  dchrvmasumlema  27444  elold  27820  lrrecfr  27892  sleadd1  27938  addsuniflem  27950  addsasslem1  27952  addsasslem2  27953  mulsuniflem  28094  addsdilem1  28096  addsdilem2  28097  mulsasslem1  28108  mulsasslem2  28109  renegscl  28406  readdscl  28407  remulscl  28410  istrkg2ld  28444  istrkg3ld  28445  1loopgrvd2  29489  wwlksnextsurj  29885  isgrpo  30484  nmo  32476  reuxfrdf  32477  rexunirn  32478  dmrab  32483  disjorf  32566  fcoinvbr  32592  mpomptxf  32666  fpwrelmapffslem  32722  1arithidom  33509  ordtconnlem1  33944  ddemeas  34256  omssubaddlem  34319  omssubadd  34320  eulerpartlemgvv  34396  bnj89  34740  bnj133  34746  bnj1019  34798  bnj1101  34803  bnj1109  34805  bnj1143  34809  bnj1198  34814  bnj1304  34838  bnj605  34926  bnj607  34935  bnj600  34938  bnj865  34942  bnj916  34952  bnj983  34970  bnj985v  34972  bnj985  34973  bnj996  34975  bnj1033  34988  bnj1083  34997  bnj1090  34998  bnj1093  34999  bnj1110  35001  bnj1128  35009  bnj1145  35012  bnj1171  35019  bnj1172  35020  bnj1174  35022  bnj1176  35024  bnj1186  35026  bnj1189  35028  bnj1253  35036  bnj1279  35037  bnj1371  35048  bnj1374  35050  bnj1312  35077  exdifsn  35098  axreg  35132  axregscl  35133  fineqvrep  35144  fineqvpow  35145  axregs  35152  lfuhgr3  35171  loop1cycl  35188  satfvsucsuc  35416  satf0op  35428  axextprim  35752  axrepprim  35753  axunprim  35754  axpowprim  35755  axregprim  35756  axinfprim  35757  axacprim  35758  dftr6  35802  coep  35803  coepr  35804  dffr5  35805  cnvco1  35810  cnvco2  35811  eldm3  35812  fundmpss  35818  dfdm5  35824  dfrn5  35825  elima4  35827  axextdfeq  35846  19.12b  35850  axextndbi  35853  brtxp  35929  brpprod  35934  brsset  35938  dfon3  35941  brtxpsd  35943  elfix  35952  dffix2  35954  sscoid  35962  dffun10  35963  elfuns  35964  elsingles  35967  snelsingles  35971  dfiota3  35972  brimg  35986  brapply  35987  brcup  35988  brcap  35989  lemsuccf  35990  funpartlem  35993  brrestrict  36000  dfrecs2  36001  dfrdg4  36002  sumeq2si  36253  prodeq2si  36255  cbvoprab2vw  36289  cbvoprab23vw  36291  cbvprodvw2  36298  neifg  36422  bj-equsexval  36711  bj-eeanvw  36764  bj-substw  36773  eliminable-abelv  36920  eliminable-abelab  36921  bj-denoteslem  36922  bj-rexvw  36931  bj-csbsnlem  36954  bj-gabima  36991  bj-snsetex  37014  bj-elsngl  37019  bj-snglc  37020  bj-abex  37081  bj-clex  37082  bj-clel3gALT  37099  bj-nul  37107  bj-dfid2ALT  37116  bj-restpw  37143  bj-restuni  37148  bj-dfmpoa  37169  bj-opabco  37239  bj-xpcossxp  37240  bj-imdirco  37241  mptsnunlem  37389  topdifinffinlem  37398  difunieq  37425  wl-dfclab  37636  poimirlem26  37692  ismblfin  37707  itg2addnclem3  37719  itg2addnc  37720  ismgmOLD  37896  sbcexfi  38163  sbccom2lem  38170  eldmres  38315  ecinn0  38391  ineleq  38392  moantr  38402  dmcnvep  38418  rnxrn  38451  rnxrnres  38452  dmsucmap  38487  dfcoss2  38521  dfcoss3  38522  cosscnv  38524  coss1cnvres  38525  coss2cnvepres  38526  1cossres  38537  cocossss  38544  rncossdmcoss  38563  eldmcoss2  38567  coss0  38587  cossid  38588  dfssr2  38597  eldmqs1cossres  38763  prtlem16  38974  prter2  38986  islshpat  39122  islpln5  39640  islvol5  39684  pmapglb  39875  polval2N  40011  cdlemftr3  40670  dibelval3  41252  dicelval3  41285  dihglb2  41447  sn-axrep5v  42315  prjspeclsp  42711  euabsn2w  42778  diophrex  42873  onsupmaxb  43337  nnoeomeqom  43410  tfsconcatlem  43434  tfsconcat0i  43443  rp-isfinite6  43616  snen1g  43622  relintab  43681  imaiun1  43749  coiun1  43750  clsk3nimkb  44138  expandexn  44387  ismnuprim  44392  rr-groth  44397  ismnushort  44399  rr-grothshortbi  44401  19.36vv  44481  19.37vv  44483  pm11.58  44488  pm11.6  44490  pm13.192  44508  2sbc5g  44514  iotasbc2  44518  onfrALTlem5  44640  onfrALTlem1  44646  ax6e2nd  44656  2sb5nd  44658  en3lplem2VD  44941  onfrALTlem5VD  44982  relopabVD  44998  ax6e2ndVD  45005  2sb5ndVD  45007  ax6e2ndALT  45027  2sb5ndALT  45029  dfac5prim  45088  brpermmodel  45101  permaxrep  45104  permac8prim  45112  rfcnnnub  45138  stoweidlem34  46137  stoweidlem35  46138  stoweidlem60  46163  smfpimcc  46911  ichexmpl1  47574  sprid  47579  dfgric2  48020  usgrgrtrirex  48055  grlimgrtri  48108  eliunxp2  48439  mosssn2  48922  coxp  48938  istermc  49580  setrec1lem3  49795  elpglem3  49819  eximp-surprise  49890