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  1917  19.41vv  1985  19.41vvv  1986  19.41vvvv  1987  exdistr  1989  exdistr2  1993  3exdistr  1995  19.12vvv  2029  excom13  2204  exrot4  2206  2sb5  2315  dfsb7  2316  eeor  2367  19.12vv  2380  eean  2381  eeeanv  2383  ee4anv  2384  2sb8ef  2388  equsexALT  2451  2sb5rf  2504  2sb8e  2562  mo4  2594  eu6lem  2601  sb8eulem  2626  cbvmovw  2630  cbvmow  2631  eu1  2638  sbmo  2642  2moswapv  2657  2moswap  2672  euae  2687  issettru  2842  issetlem  2844  clabel  2909  sbabel  2958  nabbib  3064  rextru  3097  rexbii2  3109  r2exlem  3155  r19.41v  3196  r3ex  3205  r19.41  3270  rexcom4  3293  2ex2rexrot  3301  rexv  3481  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  gencbvex  3510  spc3egv  3561  spc3gv  3562  ceqsrexv  3612  rexrab2  3661  euxfrw  3682  euxfr  3684  euind  3685  reu6  3687  reu3  3688  2reuswap  3707  2reuswap2  3708  reuind  3714  2reu5lem3  3718  2reu5  3719  2rmoswap  3722  sbcimdv  3810  sbcg  3814  rmo2  3838  rmoanim  3846  rmoanimALT  3847  rexun  4197  reupick3  4278  euelss  4280  ndisj  4321  inn0f  4322  pssnel  4427  rexsns  4633  exsnrex  4642  snprc  4680  euabsn2  4688  reusn  4690  eusn  4693  elpreqpr  4827  elunirab  4887  uniprg  4888  uniun  4895  uniinOLD  4897  uni0b  4899  uniintsn  4950  iuncom4  4965  dfiun2g  4993  iunn0  5030  iunxiun  5062  disjor  5090  cbvopab2  5187  cbvopab2v  5190  unopab  5191  axrep1  5239  axrep4v  5243  axrep4  5244  axrep5  5245  axrep6  5246  zfrep6  5248  zfrep4  5252  axsepgfromrep  5253  axnulALT  5264  0ex  5267  vnexOLD  5278  inex1  5284  inuni  5318  axpweq  5319  zfpow  5335  axpow2  5336  vpwex  5346  zfpair  5390  zfpair2  5399  prex  5403  el.OLD  5414  eqvinop  5463  eqvinot  5464  copsexgw  5467  copsexgwOLD  5468  copsexg  5469  cotsexgw  5470  opabn0  5535  iunopab  5541  dfid2  5555  dfid3  5556  opeliunxp  5725  opeliun2xp  5726  xpiundi  5729  xpiundir  5730  elvv  5733  elvvv  5735  csbxp  5760  eliunxp  5824  exopxfr  5831  relop  5838  opelco2g  5856  cnvco  5879  cnvuni  5880  dfdm3  5881  dfrn2  5882  dfrn3  5883  elrng  5885  dfdm4  5889  csbdm  5891  eldm2g  5893  dmun  5904  dmin  5905  dmiun  5907  dmuni  5908  dmopab  5909  dmi  5915  dmep  5917  rnep  5921  dmxp  5923  rnopab  5948  dmcosseq  5972  dmcosseqOLD  5973  dmres  6020  elsnres  6028  dfima2  6076  elima3  6081  imadmrnOLD  6086  imai  6090  args  6108  rniun  6157  xpdifid  6177  xpdifcnvepel  6178  ssrnres  6188  dmsnn0  6227  dmsnopg  6233  cnvresima  6250  mptpreima  6258  dfco2  6265  coundi  6267  coundir  6268  resco  6270  imaco  6271  rnco  6272  rncoOLD  6273  coiun  6277  coi1  6285  coassOLD  6291  xpco  6318  elsnxp  6320  dfpo2  6325  dffun5  6580  imadif  6654  tz6.12-2  6903  brprcneu  6906  brprcneuALT  6907  dffv2  7011  fndmin  7075  fvn0ssdmfun  7106  abrexco  7279  imaiun  7280  isomin  7376  dfoprab2  7509  cbvoprab2  7539  zfun  7784  uniex2  7786  uniex2OLD  7787  uniuni  7808  elxp4  7968  elxp5  7969  fiun  7989  f1iun  7990  f11o  7993  fvresex  8006  opabex3d  8011  opabex3rd  8012  opabex3  8013  abexssex  8016  abexex  8017  oprabrexex2  8024  releldm2  8088  dfopab2  8098  dfoprab3s  8099  fsplit  8165  frxp  8175  suppvalbr  8218  suppvalbrOLD  8219  cnvimadfsn  8227  brtpos2  8287  dfrecs3  8418  oarec  8608  oeeu  8650  domen  9026  xpsnen  9118  xpcomco  9124  xpassen  9128  inf2  9661  zfinf  9677  axinf2  9678  zfinf2  9680  brttrcl2  9752  ttrcltr  9754  ttrclresv  9755  ttrclselem2  9764  rankuni  9916  scott0b  9974  scott0OLD  9975  cp  9991  setrec1lem3  10006  ween  10153  aceq1  10235  aceq0  10236  aceq2  10237  dfac5lem1  10241  dfac5lem2  10242  dfac5lem3  10243  kmlem3  10270  kmlem14  10281  kmlem15  10282  kmlem16  10283  cflem  10362  cf0  10367  cfval2  10377  cfss  10382  cfslb  10383  fin23lem32  10461  axdc2lem  10565  zfac  10577  ac9  10600  ac9s  10610  axpowndlem3  10723  zfcndrep  10738  zfcndun  10739  zfcndpow  10740  zfcndinf  10742  zfcndac  10743  axgroth5  10948  axgroth2  10949  axgroth6  10952  axgroth3  10955  axgroth4  10956  grothprim  10958  grothtsk  10959  genpass  11133  ltexprlem1  11160  ltexprlem4  11163  supaddc  12324  supadd  12325  supmul1  12326  supmullem2  12328  2rexuz  13067  nnwos  13082  hashgt23el  14610  hashfun  14623  wwlktovfo  15154  xpcogend  15170  cbvsum  15906  cbvsumv  15907  cbvprod  16126  cbvprodv  16127  prodeq1i  16129  iprodmul  16214  maxprmfct  16929  4sqlem12  17178  vdwmc  17200  cshwrepswhash1  17324  imasleval  17763  isacs2  17877  cicsym  18029  gsumval3eu  20169  lidlnz  21581  isbasis2g  23321  tgval2  23329  ntreq0  23450  lmff  23674  cmpfi  23781  is1stc2  23815  1stcelcls  23835  unisngl  23901  isfbas2  24209  elfg  24245  alexsubALTlem3  24423  ustfilxp  24587  metrest  24898  metuel2  24939  restmetu  24944  dchrvmasumlema  27884  elold  28302  lrrecfr  28386  leadds1  28432  addsuniflem  28444  addsasslem1  28446  addsasslem2  28447  mulsuniflem  28592  addsdilem1  28594  addsdilem2  28595  mulsasslem1  28606  mulsasslem2  28607  elreno2  28938  renegscl  28941  readdscl  28942  remulscl  28945  istrkg2ld  28979  istrkg3ld  28980  lfuhgr3  29785  1loopgrvd2  30141  wwlksnextsurj  30546  loop1cycl  30801  isgrpo  31156  nmo  33185  reuxfrdf  33186  rexunirn  33187  dmrab  33192  disjorf  33271  fcoinvbr  33297  mpomptxf  33369  fpwrelmapffslem  33420  1arithidom  34173  ordtconnlem1  34667  ddemeas  34980  omssubaddlem  35042  omssubadd  35043  eulerpartlemgvv  35119  bnj89  35463  bnj133  35469  bnj1019  35521  bnj1101  35526  bnj1109  35528  bnj1143  35531  bnj1198  35536  bnj1304  35560  bnj605  35648  bnj607  35657  bnj600  35660  bnj865  35664  bnj916  35674  bnj983  35692  bnj985v  35694  bnj985  35695  bnj996  35697  bnj1033  35710  bnj1083  35719  bnj1090  35720  bnj1093  35721  bnj1110  35723  bnj1128  35731  bnj1145  35734  bnj1171  35741  bnj1172  35742  bnj1174  35744  bnj1176  35746  bnj1186  35748  bnj1189  35750  bnj1253  35758  bnj1279  35759  bnj1371  35770  bnj1374  35772  bnj1312  35799  reu6f  35820  exdifsn  35824  axnulALT2  35825  axprALT2  35857  fineqvrep  35923  fineqvpow  35924  axreg  35936  axregscl  35937  axregs  35948  axpowg  35955  onvfowev  36091  vsmrep  36131  satfvsucsuc  36338  satf0op  36350  mirimanofffr  36670  axextprim  36681  axrepprim  36682  axunprim  36683  axpowprim  36684  axregprim  36685  axinfprim  36686  axacprim  36687  dftr6  36731  coep  36732  coepr  36733  dffr5  36734  cnvco1  36739  cnvco2  36740  eldm3  36741  fundmpss  36747  dfdm5  36752  dfrn5  36753  elima4  36755  axextdfeq  36774  19.12b  36778  axextndbi  36781  brtxp  36857  brpprod  36862  brsset  36866  dfon3  36869  brtxpsd  36871  elfix  36880  dffix2  36882  sscoid  36890  dffun10  36891  elfuns  36892  elsingles  36895  snelsingles  36899  dfiota3  36900  brimg  36914  brapply  36915  brcup  36916  brcap  36917  lemsuccf  36918  funpartlem  36921  brrestrict  36928  dfrecs2  36929  dfrdg4  36930  sumeq2si  37206  prodeq2si  37208  cbvoprab2vw  37242  cbvoprab23vw  37244  cbvprodvw2  37251  neifg  37374  regsfromregtco  37541  regsfromunir1  37543  mh-prprimbi  37546  mh-unprimbi  37547  mh-infprim1bi  37549  mh-infprim2bi  37550  mh-infprim3bi  37551  bj-df-sb  37764  bj-dfsbc  37766  bj-equsexval  37774  bj-eeanvw  37832  bj-substw  37842  eliminable-abelv  37996  eliminable-abelab  37997  bj-denoteslem  37998  bj-rexvw  38007  bj-csbsnlem  38030  bj-gabima  38068  bj-snsetex  38091  bj-elsngl  38096  bj-snglc  38097  bj-abex  38158  bj-clex  38159  bj-dfres2  38185  coi1res  38199  coi2res  38200  coresrn  38204  bj-clel3gALT  38233  bj-nul  38241  bj-dfid2ALT  38250  bj-rep  38259  bj-axseprep  38260  bj-restpw  38283  bj-restuni  38288  bj-dfmpoa  38310  bj-opabco  38377  bj-xpcossxp  38378  bj-imdirco  38379  mptsnunlem  38529  topdifinffinlem  38538  difunieq  38565  wl-dfclab  38785  poimirlem26  38832  ismblfin  38847  itg2addnclem3  38859  itg2addnc  38860  negprop  38911  impprop  38912  ismgmOLD  39050  sbcexfi  39315  sbccom2lem  39322  eldmres  39475  ecinn0  39551  ineleq  39552  moantr  39570  dmcnvep  39586  rnxrn  39619  rnxrnres  39620  dmsucmap  39666  dfcoss2  39701  dfcoss3  39702  cosscnv  39704  coss1cnvres  39705  coss2cnvepres  39706  1cossres  39717  cocossss  39724  rncossdmcoss  39743  eldmcoss2  39747  coss0  39767  cossid  39768  dfssr2  39777  eldmqs1cossres  39942  prtlem16  40192  prter2  40204  islshpat  40340  islpln5  40858  islvol5  40902  pmapglb  41093  polval2N  41229  cdlemftr3  41888  dibelval3  42470  dicelval3  42503  dihglb2  42665  sn-axrep5v  43538  prjspeclsp  43906  euabsn2w  43956  diophrex  44052  onsupmaxb  44502  nnoeomeqom  44575  tfsconcatlem  44599  tfsconcat0i  44608  rp-isfinite6  44780  snen1g  44786  relintab  44845  imaiun1  44912  coiun1  44913  clsk3nimkb  45301  expandexn  45534  ismnuprim  45539  rr-groth  45544  ismnushort  45546  rr-grothshortbi  45548  19.36vv  45628  19.37vv  45630  pm11.58  45635  pm11.6  45637  pm13.192  45655  2sbc5g  45661  iotasbc2  45664  onfrALTlem5  45785  onfrALTlem1  45791  ax6e2nd  45801  2sb5nd  45803  en3lplem2VD  46086  onfrALTlem5VD  46127  relopabVD  46143  ax6e2ndVD  46150  2sb5ndVD  46152  ax6e2ndALT  46172  2sb5ndALT  46174  dfac5prim  46244  brpermmodel  46257  permaxrep  46260  permac8prim  46268  rfcnnnub  46327  stoweidlem34  47317  stoweidlem35  47318  stoweidlem60  47343  smfpimcc  48091  ichexmpl1  48824  sprid  48829  dfgric2  49286  usgrgrtrirex  49321  grlimgrtri  49374  eliunxp2  49777  mosssn2  50259  coxp  50275  istermc  50940  elpglem3  51212  eximp-surprise  51308  alsbii  51324