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  2202  exrot4  2204  2sb5  2315  dfsb7  2316  eeor  2368  19.12vv  2381  eean  2382  eeeanv  2384  ee4anv  2385  ee4anvOLD  2386  2sb8ef  2390  equsexALT  2453  2sb5rf  2506  2sb8e  2564  mo4  2596  eu6lem  2603  sb8eulem  2628  cbvmovw  2632  cbvmow  2633  eu1  2640  sbmo  2644  2moswapv  2659  2moswap  2674  euae  2689  issettru  2843  issetlem  2845  clabel  2910  sbabel  2959  nabbib  3065  rextru  3098  rexbii2  3110  r2exlem  3156  r19.41v  3197  r3ex  3206  r19.41  3271  rexcom4  3294  2ex2rexrot  3302  rexv  3484  ceqsex2  3507  ceqsex2v  3508  ceqsex3v  3509  gencbvex  3513  spc3egv  3564  spc3gv  3565  ceqsrexv  3616  rexrab2  3665  euxfrw  3686  euxfr  3688  euind  3689  reu6  3691  reu3  3692  2reuswap  3711  2reuswap2  3712  reuind  3718  2reu5lem3  3722  2reu5  3723  2rmoswap  3726  sbcimdv  3814  sbcg  3818  rmo2  3841  rmoanim  3849  rmoanimALT  3850  rexun  4149  reupick3  4283  euelss  4285  ndisj  4325  inn0f  4326  pssnel  4431  rexsns  4639  exsnrex  4648  snprc  4685  euabsn2  4693  reusn  4695  eusn  4698  elpreqpr  4834  elunirab  4889  uniprg  4890  uniun  4897  uniinOLD  4899  uni0b  4901  uniintsn  4952  iuncom4  4967  dfiun2g  4996  iunn0  5033  iunxiun  5065  disjor  5093  cbvopab2  5189  cbvopab2v  5192  unopab  5193  axrep1  5241  axrep4v  5245  axrep4  5246  axrep4OLD  5247  axrep5  5248  axrep6  5249  axrep6OLD  5250  zfrep6  5252  zfrep4  5256  axsepgfromrep  5257  axnulALT  5269  0ex  5272  vnexOLD  5283  inex1  5288  inuni  5322  axpweq  5323  zfpow  5339  axpow2  5340  vpwex  5350  zfpair  5394  zfpair2  5407  prex  5411  el.OLD  5422  eqvinop  5471  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  opabn0  5540  iunopab  5546  dfid2  5560  dfid3  5561  opeliunxp  5730  opeliun2xp  5731  xpiundi  5734  xpiundir  5735  elvvv  5739  csbxp  5764  eliunxp  5825  exopxfr  5831  relop  5838  opelco2g  5855  cnvco  5877  cnvuni  5878  dfdm3  5879  dfrn2  5880  dfrn3  5881  elrng  5883  dfdm4  5887  csbdm  5889  eldm2g  5891  dmun  5902  dmin  5903  dmiun  5905  dmuni  5906  dmopab  5907  dmi  5913  dmep  5915  rnep  5919  dmxp  5921  rnopab  5946  dmcosseq  5970  dmcosseqOLD  5971  dmres  6013  elsnres  6022  dfima2  6066  elima3  6071  imadmrn  6074  imai  6078  args  6096  rniun  6147  xpdifid  6167  xpdifcnvepel  6168  ssrnres  6178  dmsnn0  6210  dmsnopg  6216  cnvresima  6233  mptpreima  6241  dfco2  6248  coundi  6250  coundir  6251  resco  6253  imaco  6254  rnco  6255  rncoOLD  6256  coiun  6260  coi1  6266  coass  6269  xpco  6294  elsnxp  6296  dfpo2  6301  dffun5  6554  imadif  6624  tz6.12-2  6872  brprcneu  6875  brprcneuALT  6876  dffv2  6980  fndmin  7044  fvn0ssdmfun  7073  abrexco  7244  imaiun  7245  isomin  7341  dfoprab2  7474  cbvoprab2  7504  zfun  7739  uniex2  7741  uniex2OLD  7742  uniuni  7763  elxp4  7921  elxp5  7922  fiun  7942  f1iun  7943  f11o  7946  fvresex  7959  opabex3d  7964  opabex3rd  7965  opabex3  7966  abexssex  7969  abexex  7970  oprabrexex2  7977  releldm2  8042  dfopab2  8051  dfoprab3s  8052  fsplit  8114  frxp  8124  suppvalbr  8162  cnvimadfsn  8170  brtpos2  8230  dfrecs3  8361  oarec  8549  oeeu  8591  domen  8960  xpsnen  9052  xpcomco  9058  xpassen  9062  inf2  9595  zfinf  9611  axinf2  9612  zfinf2  9614  brttrcl2  9686  ttrcltr  9688  ttrclresv  9689  ttrclselem2  9698  rankuni  9838  scott0b  9869  scott0OLD  9870  cp  9886  ween  10031  aceq1  10113  aceq0  10114  aceq2  10115  dfac5lem1  10119  dfac5lem2  10120  dfac5lem3  10121  kmlem3  10148  kmlem14  10159  kmlem15  10160  kmlem16  10161  cflem  10240  cf0  10245  cfval2  10255  cfss  10260  cfslb  10261  fin23lem32  10339  axdc2lem  10443  zfac  10455  ac9  10478  ac9s  10488  axpowndlem3  10595  zfcndrep  10610  zfcndun  10611  zfcndpow  10612  zfcndinf  10614  zfcndac  10615  axgroth5  10820  axgroth2  10821  axgroth6  10824  axgroth3  10827  axgroth4  10828  grothprim  10830  grothtsk  10831  genpass  11005  ltexprlem1  11032  ltexprlem4  11035  supaddc  12193  supadd  12194  supmul1  12195  supmullem2  12197  2rexuz  12935  nnwos  12950  hashgt23el  14474  hashfun  14487  wwlktovfo  15014  xpcogend  15030  cbvsum  15765  cbvsumv  15766  cbvprod  15985  cbvprodv  15986  prodeq1i  15988  iprodmul  16075  maxprmfct  16785  4sqlem12  17033  vdwmc  17055  cshwrepswhash1  17179  imasleval  17612  isacs2  17726  cicsym  17878  gsumval3eu  19997  lidlnz  21405  isbasis2g  23134  tgval2  23142  ntreq0  23263  lmff  23487  cmpfi  23594  is1stc2  23628  1stcelcls  23647  unisngl  23713  isfbas2  24021  elfg  24057  alexsubALTlem3  24235  ustfilxp  24399  metrest  24710  metuel2  24751  restmetu  24756  dchrvmasumlema  27693  elold  28081  lrrecfr  28165  leadds1  28211  addsuniflem  28223  addsasslem1  28225  addsasslem2  28226  mulsuniflem  28371  addsdilem1  28373  addsdilem2  28374  mulsasslem1  28385  mulsasslem2  28386  elreno2  28717  renegscl  28720  readdscl  28721  remulscl  28724  istrkg2ld  28758  istrkg3ld  28759  1loopgrvd2  29882  wwlksnextsurj  30278  isgrpo  30878  nmo  32865  reuxfrdf  32866  rexunirn  32867  dmrab  32872  disjorf  32953  fcoinvbr  32979  mpomptxf  33052  fpwrelmapffslem  33106  1arithidom  33850  ordtconnlem1  34337  ddemeas  34650  omssubaddlem  34713  omssubadd  34714  eulerpartlemgvv  34790  bnj89  35134  bnj133  35140  bnj1019  35192  bnj1101  35197  bnj1109  35199  bnj1143  35202  bnj1198  35207  bnj1304  35231  bnj605  35319  bnj607  35328  bnj600  35331  bnj865  35335  bnj916  35345  bnj983  35363  bnj985v  35365  bnj985  35366  bnj996  35368  bnj1033  35381  bnj1083  35390  bnj1090  35391  bnj1093  35392  bnj1110  35394  bnj1128  35402  bnj1145  35405  bnj1171  35412  bnj1172  35413  bnj1174  35415  bnj1176  35417  bnj1186  35419  bnj1189  35421  bnj1253  35429  bnj1279  35430  bnj1371  35441  bnj1374  35443  bnj1312  35470  exdifsn  35492  axnulALT2  35493  axprALT2  35520  fineqvrep  35543  fineqvpow  35544  axreg  35556  axregscl  35557  axregs  35568  axpowg  35575  onvfowev  35616  lfuhgr3  35625  loop1cycl  35642  satfvsucsuc  35870  satf0op  35882  axextprim  36206  axrepprim  36207  axunprim  36208  axpowprim  36209  axregprim  36210  axinfprim  36211  axacprim  36212  dftr6  36256  coep  36257  coepr  36258  dffr5  36259  cnvco1  36264  cnvco2  36265  eldm3  36266  fundmpss  36272  dfdm5  36278  dfrn5  36279  elima4  36281  axextdfeq  36300  19.12b  36304  axextndbi  36307  brtxp  36383  brpprod  36388  brsset  36392  dfon3  36395  brtxpsd  36397  elfix  36406  dffix2  36408  sscoid  36416  dffun10  36417  elfuns  36418  elsingles  36421  snelsingles  36425  dfiota3  36426  brimg  36440  brapply  36441  brcup  36442  brcap  36443  lemsuccf  36444  funpartlem  36447  brrestrict  36454  dfrecs2  36455  dfrdg4  36456  sumeq2si  36747  prodeq2si  36749  cbvoprab2vw  36783  cbvoprab23vw  36785  cbvprodvw2  36792  neifg  36915  regsfromregtco  37082  regsfromunir1  37084  mh-prprimbi  37087  mh-unprimbi  37088  mh-infprim1bi  37090  mh-infprim2bi  37091  mh-infprim3bi  37092  bj-df-sb  37305  bj-dfsbc  37307  bj-equsexval  37315  bj-eeanvw  37373  bj-substw  37383  eliminable-abelv  37537  eliminable-abelab  37538  bj-denoteslem  37539  bj-rexvw  37548  bj-csbsnlem  37571  bj-gabima  37609  bj-snsetex  37632  bj-elsngl  37637  bj-snglc  37638  bj-abex  37699  bj-clex  37700  bj-clel3gALT  37717  bj-nul  37725  bj-dfid2ALT  37734  bj-rep  37743  bj-axseprep  37744  bj-restpw  37767  bj-restuni  37772  bj-dfmpoa  37793  bj-opabco  37865  bj-xpcossxp  37866  bj-imdirco  37867  mptsnunlem  38017  topdifinffinlem  38026  difunieq  38053  wl-dfclab  38273  poimirlem26  38330  ismblfin  38345  itg2addnclem3  38357  itg2addnc  38358  ismgmOLD  38534  sbcexfi  38799  sbccom2lem  38806  eldmres  38959  ecinn0  39035  ineleq  39036  moantr  39054  dmcnvep  39070  rnxrn  39103  rnxrnres  39104  dmsucmap  39150  dfcoss2  39185  dfcoss3  39186  cosscnv  39188  coss1cnvres  39189  coss2cnvepres  39190  1cossres  39201  cocossss  39208  rncossdmcoss  39227  eldmcoss2  39231  coss0  39251  cossid  39252  dfssr2  39261  eldmqs1cossres  39426  prtlem16  39676  prter2  39688  islshpat  39824  islpln5  40342  islvol5  40386  pmapglb  40577  polval2N  40713  cdlemftr3  41372  dibelval3  41954  dicelval3  41987  dihglb2  42149  sn-axrep5v  43021  prjspeclsp  43377  euabsn2w  43444  diophrex  43539  onsupmaxb  43999  nnoeomeqom  44072  tfsconcatlem  44096  tfsconcat0i  44105  rp-isfinite6  44277  snen1g  44283  relintab  44342  imaiun1  44410  coiun1  44411  clsk3nimkb  44799  expandexn  45032  ismnuprim  45037  rr-groth  45042  ismnushort  45044  rr-grothshortbi  45046  19.36vv  45126  19.37vv  45128  pm11.58  45133  pm11.6  45135  pm13.192  45153  2sbc5g  45159  iotasbc2  45163  onfrALTlem5  45284  onfrALTlem1  45290  ax6e2nd  45300  2sb5nd  45302  en3lplem2VD  45585  onfrALTlem5VD  45626  relopabVD  45642  ax6e2ndVD  45649  2sb5ndVD  45651  ax6e2ndALT  45671  2sb5ndALT  45673  dfac5prim  45732  brpermmodel  45745  permaxrep  45748  permac8prim  45756  rfcnnnub  45789  stoweidlem34  46781  stoweidlem35  46782  stoweidlem60  46807  smfpimcc  47555  ichexmpl1  48251  sprid  48256  dfgric2  48713  usgrgrtrirex  48748  grlimgrtri  48801  eliunxp2  49147  mosssn2  49628  coxp  49644  istermc  50285  setrec1lem3  50500  elpglem3  50524  eximp-surprise  50595  alsbii  50611