Theorem exbii 1881

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

This proof depends on syntax axioms:   ↔ wb 209  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  2exbii  1882  3exbii  1883  exanali  1892  exancom  1894  19.43  1915  19.41vv  1983  19.41vvv  1984  19.41vvvv  1985  exdistr  1987  exdistr2  1991  3exdistr  1993  19.12vvv  2027  excom13  2201  exrot4  2203  2sb5  2312  dfsb7  2313  eeor  2364  19.12vv  2377  eean  2378  eeeanv  2380  ee4anv  2381  ee4anvOLD  2382  2sb8ef  2386  equsexALT  2449  2sb5rf  2502  2sb8e  2560  mo4  2592  eu6lem  2599  sb8eulem  2624  cbvmovw  2628  cbvmow  2629  eu1  2636  sbmo  2640  2moswapv  2655  2moswap  2670  euae  2685  issettru  2839  issetlem  2841  clabel  2906  sbabel  2955  nabbib  3061  rextru  3094  rexbii2  3106  r2exlem  3152  r19.41v  3193  r3ex  3202  r19.41  3267  rexcom4  3290  2ex2rexrot  3298  rexv  3478  ceqsex2  3501  ceqsex2v  3502  ceqsex3v  3503  gencbvex  3507  spc3egv  3558  spc3gv  3559  ceqsrexv  3609  rexrab2  3658  euxfrw  3679  euxfr  3681  euind  3682  reu6  3684  reu3  3685  2reuswap  3704  2reuswap2  3705  reuind  3711  2reu5lem3  3715  2reu5  3716  2rmoswap  3719  sbcimdv  3807  sbcg  3811  rmo2  3834  rmoanim  3842  rmoanimALT  3843  rexun  4142  reupick3  4276  euelss  4278  ndisj  4318  inn0f  4319  pssnel  4424  rexsns  4632  exsnrex  4641  snprc  4678  euabsn2  4686  reusn  4688  eusn  4691  elpreqpr  4827  elunirab  4882  uniprg  4883  uniun  4890  uniinOLD  4892  uni0b  4894  uniintsn  4945  iuncom4  4960  dfiun2g  4988  iunn0  5025  iunxiun  5057  disjor  5085  cbvopab2  5181  cbvopab2v  5184  unopab  5185  axrep1  5233  axrep4v  5237  axrep4  5238  axrep5  5239  axrep6  5240  zfrep6  5242  zfrep4  5246  axsepgfromrep  5247  axnulALT  5258  0ex  5261  vnexOLD  5272  inex1  5277  inuni  5311  axpweq  5312  zfpow  5328  axpow2  5329  vpwex  5339  zfpair  5383  zfpair2  5392  prex  5396  el.OLD  5407  eqvinop  5456  eqvinot  5457  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  opabn0  5528  iunopab  5534  dfid2  5548  dfid3  5549  opeliunxp  5718  opeliun2xp  5719  xpiundi  5722  xpiundir  5723  elvvv  5727  csbxp  5752  eliunxp  5814  exopxfr  5821  relop  5828  opelco2g  5845  cnvco  5867  cnvuni  5868  dfdm3  5869  dfrn2  5870  dfrn3  5871  elrng  5873  dfdm4  5877  csbdm  5879  eldm2g  5881  dmun  5892  dmin  5893  dmiun  5895  dmuni  5896  dmopab  5897  dmi  5903  dmep  5905  rnep  5909  dmxp  5911  rnopab  5936  dmcosseq  5960  dmcosseqOLD  5961  dmres  6003  elsnres  6010  dfima2  6058  elima3  6063  imadmrnOLD  6068  imai  6072  args  6090  rniun  6139  xpdifid  6159  xpdifcnvepel  6160  ssrnres  6170  dmsnn0  6207  dmsnopg  6213  cnvresima  6230  mptpreima  6238  dfco2  6245  coundi  6247  coundir  6248  resco  6250  imaco  6251  rnco  6252  rncoOLD  6253  coiun  6257  coi1  6263  coass  6266  xpco  6291  elsnxp  6293  dfpo2  6298  dffun5  6551  imadif  6622  tz6.12-2  6870  brprcneu  6873  brprcneuALT  6874  dffv2  6978  fndmin  7042  fvn0ssdmfun  7072  abrexco  7246  imaiun  7247  isomin  7343  dfoprab2  7476  cbvoprab2  7506  zfun  7750  uniex2  7752  uniex2OLD  7753  uniuni  7774  elxp4  7932  elxp5  7933  fiun  7953  f1iun  7954  f11o  7957  fvresex  7970  opabex3d  7975  opabex3rd  7976  opabex3  7977  abexssex  7980  abexex  7981  oprabrexex2  7988  releldm2  8052  dfopab2  8061  dfoprab3s  8062  fsplit  8126  frxp  8136  suppvalbr  8174  cnvimadfsn  8182  brtpos2  8242  dfrecs3  8373  oarec  8563  oeeu  8605  domen  8981  xpsnen  9073  xpcomco  9079  xpassen  9083  inf2  9617  zfinf  9633  axinf2  9634  zfinf2  9636  brttrcl2  9708  ttrcltr  9710  ttrclresv  9711  ttrclselem2  9720  rankuni  9872  scott0b  9930  scott0OLD  9931  cp  9947  setrec1lem3  9962  ween  10107  aceq1  10189  aceq0  10190  aceq2  10191  dfac5lem1  10195  dfac5lem2  10196  dfac5lem3  10197  kmlem3  10224  kmlem14  10235  kmlem15  10236  kmlem16  10237  cflem  10316  cf0  10321  cfval2  10331  cfss  10336  cfslb  10337  fin23lem32  10415  axdc2lem  10519  zfac  10531  ac9  10554  ac9s  10564  axpowndlem3  10677  zfcndrep  10692  zfcndun  10693  zfcndpow  10694  zfcndinf  10696  zfcndac  10697  axgroth5  10902  axgroth2  10903  axgroth6  10906  axgroth3  10909  axgroth4  10910  grothprim  10912  grothtsk  10913  genpass  11087  ltexprlem1  11114  ltexprlem4  11117  supaddc  12277  supadd  12278  supmul1  12279  supmullem2  12281  2rexuz  13020  nnwos  13035  hashgt23el  14562  hashfun  14575  wwlktovfo  15104  xpcogend  15120  cbvsum  15855  cbvsumv  15856  cbvprod  16075  cbvprodv  16076  prodeq1i  16078  iprodmul  16163  maxprmfct  16878  4sqlem12  17127  vdwmc  17149  cshwrepswhash1  17273  imasleval  17706  isacs2  17820  cicsym  17972  gsumval3eu  20111  lidlnz  21523  isbasis2g  23259  tgval2  23267  ntreq0  23388  lmff  23612  cmpfi  23719  is1stc2  23753  1stcelcls  23773  unisngl  23839  isfbas2  24147  elfg  24183  alexsubALTlem3  24361  ustfilxp  24525  metrest  24836  metuel2  24877  restmetu  24882  dchrvmasumlema  27820  elold  28238  lrrecfr  28322  leadds1  28368  addsuniflem  28380  addsasslem1  28382  addsasslem2  28383  mulsuniflem  28528  addsdilem1  28530  addsdilem2  28531  mulsasslem1  28542  mulsasslem2  28543  elreno2  28874  renegscl  28877  readdscl  28878  remulscl  28881  istrkg2ld  28915  istrkg3ld  28916  lfuhgr3  29721  1loopgrvd2  30077  wwlksnextsurj  30482  loop1cycl  30737  isgrpo  31092  nmo  33079  reuxfrdf  33080  rexunirn  33081  dmrab  33086  disjorf  33166  fcoinvbr  33192  mpomptxf  33265  fpwrelmapffslem  33317  1arithidom  34062  ordtconnlem1  34549  ddemeas  34862  omssubaddlem  34924  omssubadd  34925  eulerpartlemgvv  35001  bnj89  35345  bnj133  35351  bnj1019  35403  bnj1101  35408  bnj1109  35410  bnj1143  35413  bnj1198  35418  bnj1304  35442  bnj605  35530  bnj607  35539  bnj600  35542  bnj865  35546  bnj916  35556  bnj983  35574  bnj985v  35576  bnj985  35577  bnj996  35579  bnj1033  35592  bnj1083  35601  bnj1090  35602  bnj1093  35603  bnj1110  35605  bnj1128  35613  bnj1145  35616  bnj1171  35623  bnj1172  35624  bnj1174  35626  bnj1176  35628  bnj1186  35630  bnj1189  35632  bnj1253  35640  bnj1279  35641  bnj1371  35652  bnj1374  35654  bnj1312  35681  exdifsn  35703  axnulALT2  35704  axprALT2  35723  fineqvrep  35765  fineqvpow  35766  axreg  35778  axregscl  35779  axregs  35790  axpowg  35797  onvfowev  35878  satfvsucsuc  36109  satf0op  36121  axextprim  36445  axrepprim  36446  axunprim  36447  axpowprim  36448  axregprim  36449  axinfprim  36450  axacprim  36451  dftr6  36495  coep  36496  coepr  36497  dffr5  36498  cnvco1  36503  cnvco2  36504  eldm3  36505  fundmpss  36511  dfdm5  36517  dfrn5  36518  elima4  36520  axextdfeq  36539  19.12b  36543  axextndbi  36546  brtxp  36622  brpprod  36627  brsset  36631  dfon3  36634  brtxpsd  36636  elfix  36645  dffix2  36647  sscoid  36655  dffun10  36656  elfuns  36657  elsingles  36660  snelsingles  36664  dfiota3  36665  brimg  36679  brapply  36680  brcup  36681  brcap  36682  lemsuccf  36683  funpartlem  36686  brrestrict  36693  dfrecs2  36694  dfrdg4  36695  sumeq2si  36971  prodeq2si  36973  cbvoprab2vw  37007  cbvoprab23vw  37009  cbvprodvw2  37016  neifg  37139  regsfromregtco  37306  regsfromunir1  37308  mh-prprimbi  37311  mh-unprimbi  37312  mh-infprim1bi  37314  mh-infprim2bi  37315  mh-infprim3bi  37316  bj-df-sb  37529  bj-dfsbc  37531  bj-equsexval  37539  bj-eeanvw  37597  bj-substw  37607  eliminable-abelv  37761  eliminable-abelab  37762  bj-denoteslem  37763  bj-rexvw  37772  bj-csbsnlem  37795  bj-gabima  37833  bj-snsetex  37856  bj-elsngl  37861  bj-snglc  37862  bj-abex  37923  bj-clex  37924  coi1in  37941  bj-clel3gALT  37943  bj-nul  37951  bj-dfid2ALT  37960  bj-rep  37969  bj-axseprep  37970  bj-restpw  37993  bj-restuni  37998  bj-dfmpoa  38019  bj-opabco  38089  bj-xpcossxp  38090  bj-imdirco  38091  mptsnunlem  38241  topdifinffinlem  38250  difunieq  38277  wl-dfclab  38497  poimirlem26  38544  ismblfin  38559  itg2addnclem3  38571  itg2addnc  38572  negprop  38623  impprop  38624  ismgmOLD  38764  sbcexfi  39029  sbccom2lem  39036  eldmres  39189  ecinn0  39265  ineleq  39266  moantr  39284  dmcnvep  39300  rnxrn  39333  rnxrnres  39334  dmsucmap  39380  dfcoss2  39415  dfcoss3  39416  cosscnv  39418  coss1cnvres  39419  coss2cnvepres  39420  1cossres  39431  cocossss  39438  rncossdmcoss  39457  eldmcoss2  39461  coss0  39481  cossid  39482  dfssr2  39491  eldmqs1cossres  39656  prtlem16  39906  prter2  39918  islshpat  40054  islpln5  40572  islvol5  40616  pmapglb  40807  polval2N  40943  cdlemftr3  41602  dibelval3  42184  dicelval3  42217  dihglb2  42379  sn-axrep5v  43251  prjspeclsp  43620  euabsn2w  43670  diophrex  43765  onsupmaxb  44225  nnoeomeqom  44298  tfsconcatlem  44322  tfsconcat0i  44331  rp-isfinite6  44503  snen1g  44509  relintab  44568  imaiun1  44636  coiun1  44637  clsk3nimkb  45025  expandexn  45258  ismnuprim  45263  rr-groth  45268  ismnushort  45270  rr-grothshortbi  45272  19.36vv  45352  19.37vv  45354  pm11.58  45359  pm11.6  45361  pm13.192  45379  2sbc5g  45385  iotasbc2  45389  onfrALTlem5  45510  onfrALTlem1  45516  ax6e2nd  45526  2sb5nd  45528  en3lplem2VD  45811  onfrALTlem5VD  45852  relopabVD  45868  ax6e2ndVD  45875  2sb5ndVD  45877  ax6e2ndALT  45897  2sb5ndALT  45899  dfac5prim  45958  brpermmodel  45971  permaxrep  45974  permac8prim  45982  rfcnnnub  46022  stoweidlem34  47013  stoweidlem35  47014  stoweidlem60  47039  smfpimcc  47787  ichexmpl1  48520  sprid  48525  dfgric2  48982  usgrgrtrirex  49017  grlimgrtri  49070  eliunxp2  49415  mosssn2  49896  coxp  49912  istermc  50551  elpglem3  50775  eximp-surprise  50849  alsbii  50865