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  2311  dfsb7  2312  eeor  2363  19.12vv  2376  eean  2377  eeeanv  2379  ee4anv  2380  ee4anvOLD  2381  2sb8ef  2385  equsexALT  2448  2sb5rf  2501  2sb8e  2559  mo4  2591  eu6lem  2598  sb8eulem  2623  cbvmovw  2627  cbvmow  2628  eu1  2635  sbmo  2639  2moswapv  2654  2moswap  2669  euae  2684  issettru  2838  issetlem  2840  clabel  2905  sbabel  2954  nabbib  3060  rextru  3093  rexbii2  3105  r2exlem  3151  r19.41v  3192  r3ex  3201  r19.41  3266  rexcom4  3289  2ex2rexrot  3297  rexv  3477  ceqsex2  3500  ceqsex2v  3501  ceqsex3v  3502  gencbvex  3506  spc3egv  3557  spc3gv  3558  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  axrep4OLD  5239  axrep5  5240  axrep6  5241  axrep6OLD  5242  zfrep6  5244  zfrep4  5248  axsepgfromrep  5249  axnulALT  5261  0ex  5264  vnexOLD  5275  inex1  5280  inuni  5314  axpweq  5315  zfpow  5331  axpow2  5332  vpwex  5342  zfpair  5386  zfpair2  5399  prex  5403  el.OLD  5414  eqvinop  5463  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  opabn0  5532  iunopab  5538  dfid2  5552  dfid3  5553  opeliunxp  5722  opeliun2xp  5723  xpiundi  5726  xpiundir  5727  elvvv  5731  csbxp  5756  eliunxp  5817  exopxfr  5823  relop  5830  opelco2g  5847  cnvco  5869  cnvuni  5870  dfdm3  5871  dfrn2  5872  dfrn3  5873  elrng  5875  dfdm4  5879  csbdm  5881  eldm2g  5883  dmun  5894  dmin  5895  dmiun  5897  dmuni  5898  dmopab  5899  dmi  5905  dmep  5907  rnep  5911  dmxp  5913  rnopab  5938  dmcosseq  5962  dmcosseqOLD  5963  dmres  6005  elsnres  6014  dfima2  6058  elima3  6063  imadmrn  6066  imai  6070  args  6088  rniun  6139  xpdifid  6160  xpdifcnvepel  6161  ssrnres  6171  dmsnn0  6203  dmsnopg  6209  cnvresima  6226  mptpreima  6234  dfco2  6241  coundi  6243  coundir  6244  resco  6246  imaco  6247  rnco  6248  rncoOLD  6249  coiun  6253  coi1  6259  coass  6262  xpco  6287  elsnxp  6289  dfpo2  6294  dffun5  6547  imadif  6617  tz6.12-2  6865  brprcneu  6868  brprcneuALT  6869  dffv2  6973  fndmin  7037  fvn0ssdmfun  7067  abrexco  7241  imaiun  7242  isomin  7338  dfoprab2  7471  cbvoprab2  7501  zfun  7737  uniex2  7739  uniex2OLD  7740  uniuni  7761  elxp4  7919  elxp5  7920  fiun  7940  f1iun  7941  f11o  7944  fvresex  7957  opabex3d  7962  opabex3rd  7963  opabex3  7964  abexssex  7967  abexex  7968  oprabrexex2  7975  releldm2  8040  dfopab2  8049  dfoprab3s  8050  fsplit  8114  frxp  8124  suppvalbr  8162  cnvimadfsn  8170  brtpos2  8230  dfrecs3  8361  oarec  8549  oeeu  8591  domen  8967  xpsnen  9059  xpcomco  9065  xpassen  9069  inf2  9602  zfinf  9618  axinf2  9619  zfinf2  9621  brttrcl2  9693  ttrcltr  9695  ttrclresv  9696  ttrclselem2  9705  rankuni  9845  scott0b  9876  scott0OLD  9877  cp  9893  ween  10038  aceq1  10120  aceq0  10121  aceq2  10122  dfac5lem1  10126  dfac5lem2  10127  dfac5lem3  10128  kmlem3  10155  kmlem14  10166  kmlem15  10167  kmlem16  10168  cflem  10247  cf0  10252  cfval2  10262  cfss  10267  cfslb  10268  fin23lem32  10346  axdc2lem  10450  zfac  10462  ac9  10485  ac9s  10495  axpowndlem3  10608  zfcndrep  10623  zfcndun  10624  zfcndpow  10625  zfcndinf  10627  zfcndac  10628  axgroth5  10833  axgroth2  10834  axgroth6  10837  axgroth3  10840  axgroth4  10841  grothprim  10843  grothtsk  10844  genpass  11018  ltexprlem1  11045  ltexprlem4  11048  supaddc  12206  supadd  12207  supmul1  12208  supmullem2  12210  2rexuz  12949  nnwos  12964  hashgt23el  14489  hashfun  14502  wwlktovfo  15031  xpcogend  15047  cbvsum  15782  cbvsumv  15783  cbvprod  16002  cbvprodv  16003  prodeq1i  16005  iprodmul  16090  maxprmfct  16800  4sqlem12  17048  vdwmc  17070  cshwrepswhash1  17194  imasleval  17627  isacs2  17741  cicsym  17893  gsumval3eu  20031  lidlnz  21439  isbasis2g  23173  tgval2  23181  ntreq0  23302  lmff  23526  cmpfi  23633  is1stc2  23667  1stcelcls  23687  unisngl  23753  isfbas2  24061  elfg  24097  alexsubALTlem3  24275  ustfilxp  24439  metrest  24750  metuel2  24791  restmetu  24796  dchrvmasumlema  27736  elold  28124  lrrecfr  28208  leadds1  28254  addsuniflem  28266  addsasslem1  28268  addsasslem2  28269  mulsuniflem  28414  addsdilem1  28416  addsdilem2  28417  mulsasslem1  28428  mulsasslem2  28429  elreno2  28760  renegscl  28763  readdscl  28764  remulscl  28767  istrkg2ld  28801  istrkg3ld  28802  lfuhgr3  29607  1loopgrvd2  29963  wwlksnextsurj  30368  loop1cycl  30623  isgrpo  30978  nmo  32965  reuxfrdf  32966  rexunirn  32967  dmrab  32972  disjorf  33052  fcoinvbr  33078  mpomptxf  33151  fpwrelmapffslem  33203  1arithidom  33947  ordtconnlem1  34434  ddemeas  34747  omssubaddlem  34810  omssubadd  34811  eulerpartlemgvv  34887  bnj89  35231  bnj133  35237  bnj1019  35289  bnj1101  35294  bnj1109  35296  bnj1143  35299  bnj1198  35304  bnj1304  35328  bnj605  35416  bnj607  35425  bnj600  35428  bnj865  35432  bnj916  35442  bnj983  35460  bnj985v  35462  bnj985  35463  bnj996  35465  bnj1033  35478  bnj1083  35487  bnj1090  35488  bnj1093  35489  bnj1110  35491  bnj1128  35499  bnj1145  35502  bnj1171  35509  bnj1172  35510  bnj1174  35512  bnj1176  35514  bnj1186  35516  bnj1189  35518  bnj1253  35526  bnj1279  35527  bnj1371  35538  bnj1374  35540  bnj1312  35567  exdifsn  35589  axnulALT2  35590  axprALT2  35617  fineqvrep  35640  fineqvpow  35641  axreg  35653  axregscl  35654  axregs  35665  axpowg  35672  onvfowev  35713  satfvsucsuc  35944  satf0op  35956  axextprim  36280  axrepprim  36281  axunprim  36282  axpowprim  36283  axregprim  36284  axinfprim  36285  axacprim  36286  dftr6  36330  coep  36331  coepr  36332  dffr5  36333  cnvco1  36338  cnvco2  36339  eldm3  36340  fundmpss  36346  dfdm5  36352  dfrn5  36353  elima4  36355  axextdfeq  36374  19.12b  36378  axextndbi  36381  brtxp  36457  brpprod  36462  brsset  36466  dfon3  36469  brtxpsd  36471  elfix  36480  dffix2  36482  sscoid  36490  dffun10  36491  elfuns  36492  elsingles  36495  snelsingles  36499  dfiota3  36500  brimg  36514  brapply  36515  brcup  36516  brcap  36517  lemsuccf  36518  funpartlem  36521  brrestrict  36528  dfrecs2  36529  dfrdg4  36530  sumeq2si  36822  prodeq2si  36824  cbvoprab2vw  36858  cbvoprab23vw  36860  cbvprodvw2  36867  neifg  36990  regsfromregtco  37157  regsfromunir1  37159  mh-prprimbi  37162  mh-unprimbi  37163  mh-infprim1bi  37165  mh-infprim2bi  37166  mh-infprim3bi  37167  bj-df-sb  37380  bj-dfsbc  37382  bj-equsexval  37390  bj-eeanvw  37448  bj-substw  37458  eliminable-abelv  37612  eliminable-abelab  37613  bj-denoteslem  37614  bj-rexvw  37623  bj-csbsnlem  37646  bj-gabima  37684  bj-snsetex  37707  bj-elsngl  37712  bj-snglc  37713  bj-abex  37774  bj-clex  37775  bj-clel3gALT  37792  bj-nul  37800  bj-dfid2ALT  37809  bj-rep  37818  bj-axseprep  37819  bj-restpw  37842  bj-restuni  37847  bj-dfmpoa  37868  bj-opabco  37940  bj-xpcossxp  37941  bj-imdirco  37942  mptsnunlem  38092  topdifinffinlem  38101  difunieq  38128  wl-dfclab  38348  poimirlem26  38395  ismblfin  38410  itg2addnclem3  38422  itg2addnc  38423  ismgmOLD  38600  sbcexfi  38865  sbccom2lem  38872  eldmres  39025  ecinn0  39101  ineleq  39102  moantr  39120  dmcnvep  39136  rnxrn  39169  rnxrnres  39170  dmsucmap  39216  dfcoss2  39251  dfcoss3  39252  cosscnv  39254  coss1cnvres  39255  coss2cnvepres  39256  1cossres  39267  cocossss  39274  rncossdmcoss  39293  eldmcoss2  39297  coss0  39317  cossid  39318  dfssr2  39327  eldmqs1cossres  39492  prtlem16  39742  prter2  39754  islshpat  39890  islpln5  40408  islvol5  40452  pmapglb  40643  polval2N  40779  cdlemftr3  41438  dibelval3  42020  dicelval3  42053  dihglb2  42215  sn-axrep5v  43087  prjspeclsp  43458  euabsn2w  43525  diophrex  43620  onsupmaxb  44080  nnoeomeqom  44153  tfsconcatlem  44177  tfsconcat0i  44186  rp-isfinite6  44358  snen1g  44364  relintab  44423  imaiun1  44491  coiun1  44492  clsk3nimkb  44880  expandexn  45113  ismnuprim  45118  rr-groth  45123  ismnushort  45125  rr-grothshortbi  45127  19.36vv  45207  19.37vv  45209  pm11.58  45214  pm11.6  45216  pm13.192  45234  2sbc5g  45240  iotasbc2  45244  onfrALTlem5  45365  onfrALTlem1  45371  ax6e2nd  45381  2sb5nd  45383  en3lplem2VD  45666  onfrALTlem5VD  45707  relopabVD  45723  ax6e2ndVD  45730  2sb5ndVD  45732  ax6e2ndALT  45752  2sb5ndALT  45754  dfac5prim  45813  brpermmodel  45826  permaxrep  45829  permac8prim  45837  rfcnnnub  45870  stoweidlem34  46862  stoweidlem35  46863  stoweidlem60  46888  smfpimcc  47636  ichexmpl1  48369  sprid  48374  dfgric2  48831  usgrgrtrirex  48866  grlimgrtri  48919  eliunxp2  49264  mosssn2  49745  coxp  49761  istermc  50400  setrec1lem3  50615  elpglem3  50639  eximp-surprise  50713  alsbii  50729