Theorem exbii 1878

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

Syntax hints:   ↔ wb 209  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  2exbii  1879  3exbii  1880  exanali  1889  exancom  1891  19.43  1912  19.41vv  1980  19.41vvv  1981  19.41vvvv  1982  exdistr  1984  exdistr2  1988  3exdistr  1990  19.12vvv  2024  excom13  2199  exrot4  2201  2sb5  2313  dfsb7  2314  eeor  2366  19.12vv  2379  eean  2380  eeeanv  2382  ee4anv  2383  ee4anvOLD  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  2841  issetlem  2843  clabel  2908  sbabel  2957  nabbib  3063  rextru  3096  rexbii2  3108  r2exlem  3154  r19.41v  3195  r3ex  3204  r19.41  3269  rexcom4  3292  2ex2rexrot  3300  rexv  3482  ceqsex2  3505  ceqsex2v  3506  ceqsex3v  3507  gencbvex  3511  spc3egv  3563  spc3gv  3564  ceqsrexv  3615  rexrab2  3664  euxfrw  3685  euxfr  3687  euind  3688  reu6  3690  reu3  3691  2reuswap  3710  2reuswap2  3711  reuind  3717  2reu5lem3  3721  2reu5  3722  2rmoswap  3725  sbcimdv  3813  sbcg  3817  sbccomlemOLD  3824  rmo2  3841  rmoanim  3849  rmoanimALT  3850  rexun  4150  reupick3  4284  euelss  4286  ndisj  4326  inn0f  4327  pssnel  4432  rexsns  4638  exsnrex  4647  snprc  4684  euabsn2  4692  reusn  4694  eusn  4697  elpreqpr  4833  elunirab  4888  uniprg  4889  uniun  4896  uniinOLD  4898  uni0b  4900  uniintsn  4951  iuncom4  4966  dfiun2g  4995  iunn0  5032  iunxiun  5064  disjor  5092  cbvopab2  5188  cbvopab2v  5191  unopab  5192  axrep1  5240  axrep4v  5244  axrep4  5245  axrep4OLD  5246  axrep5  5247  axrep6  5248  axrep6OLD  5249  zfrep6  5251  zfrep4  5255  axsepgfromrep  5256  axnulALT  5268  0ex  5271  vnexOLD  5282  inex1  5287  inuni  5322  axpweq  5323  zfpow  5339  axpow2  5340  vpwex  5350  zfpair  5394  zfpair2  5407  prex  5411  elOLD  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  6292  elsnxp  6294  dfpo2  6299  dffun5  6552  imadif  6622  tz6.12-2  6870  brprcneu  6873  brprcneuALT  6874  dffv2  6978  fndmin  7042  fvn0ssdmfun  7071  abrexco  7244  imaiun  7245  isomin  7337  imaeqsexvOLD  7363  dfoprab2  7470  cbvoprab2  7500  zfun  7735  uniex2  7737  uniex2OLD  7738  uniuni  7762  elxp4  7920  elxp5  7921  fiun  7941  f1iun  7942  f11o  7945  fvresex  7958  opabex3d  7963  opabex3rd  7964  opabex3  7965  abexssex  7968  abexex  7969  oprabrexex2  7976  releldm2  8041  dfopab2  8050  dfoprab3s  8051  fsplit  8113  frxp  8123  suppvalbr  8161  cnvimadfsn  8169  brtpos2  8229  dfrecs3  8360  oarec  8548  oeeu  8590  domen  8959  xpsnen  9050  xpcomco  9056  xpassen  9060  inf2  9593  zfinf  9609  axinf2  9610  zfinf2  9612  brttrcl2  9684  ttrcltr  9686  ttrclresv  9687  ttrclselem2  9696  rankuni  9836  scott0  9861  cp  9878  ween  10020  aceq1  10102  aceq0  10103  aceq2  10104  dfac5lem1  10108  dfac5lem2  10109  dfac5lem3  10110  kmlem3  10137  kmlem14  10148  kmlem15  10149  kmlem16  10150  cflem  10229  cflemOLD  10230  cf0  10235  cfval2  10245  cfss  10250  cfslb  10251  fin23lem32  10329  axdc2lem  10433  zfac  10445  ac9  10468  ac9s  10478  axpowndlem3  10585  zfcndrep  10600  zfcndun  10601  zfcndpow  10602  zfcndinf  10604  zfcndac  10605  axgroth5  10810  axgroth2  10811  axgroth6  10814  axgroth3  10817  axgroth4  10818  grothprim  10820  grothtsk  10821  genpass  10995  ltexprlem1  11022  ltexprlem4  11025  supaddc  12183  supadd  12184  supmul1  12185  supmullem2  12187  2rexuz  12925  nnwos  12940  hashgt23el  14463  hashfun  14476  wwlktovfo  14997  xpcogend  15013  cbvsum  15748  cbvsumv  15749  cbvprod  15969  cbvprodv  15970  prodeq1i  15972  iprodmul  16059  maxprmfct  16769  4sqlem12  17017  vdwmc  17039  cshwrepswhash1  17163  imasleval  17596  isacs2  17710  cicsym  17862  gsumval3eu  19975  lidlnz  21357  isbasis2g  23086  tgval2  23094  ntreq0  23215  lmff  23439  cmpfi  23546  is1stc2  23580  1stcelcls  23599  unisngl  23665  isfbas2  23973  elfg  24009  alexsubALTlem3  24187  ustfilxp  24351  metrest  24662  metuel2  24703  restmetu  24708  dchrvmasumlema  27645  elold  28033  lrrecfr  28117  leadds1  28163  addsuniflem  28175  addsasslem1  28177  addsasslem2  28178  mulsuniflem  28323  addsdilem1  28325  addsdilem2  28326  mulsasslem1  28337  mulsasslem2  28338  elreno2  28669  renegscl  28672  readdscl  28673  remulscl  28676  istrkg2ld  28710  istrkg3ld  28711  1loopgrvd2  29834  wwlksnextsurj  30230  isgrpo  30830  nmo  32817  reuxfrdf  32818  rexunirn  32819  dmrab  32824  disjorf  32905  fcoinvbr  32931  mpomptxf  33004  fpwrelmapffslem  33058  1arithidom  33808  ordtconnlem1  34295  ddemeas  34607  omssubaddlem  34670  omssubadd  34671  eulerpartlemgvv  34747  bnj89  35091  bnj133  35097  bnj1019  35149  bnj1101  35154  bnj1109  35156  bnj1143  35159  bnj1198  35164  bnj1304  35188  bnj605  35276  bnj607  35285  bnj600  35288  bnj865  35292  bnj916  35302  bnj983  35320  bnj985v  35322  bnj985  35323  bnj996  35325  bnj1033  35338  bnj1083  35347  bnj1090  35348  bnj1093  35349  bnj1110  35351  bnj1128  35359  bnj1145  35362  bnj1171  35369  bnj1172  35370  bnj1174  35372  bnj1176  35374  bnj1186  35376  bnj1189  35378  bnj1253  35386  bnj1279  35387  bnj1371  35398  bnj1374  35400  bnj1312  35427  exdifsn  35449  axnulALT2  35452  axprALT2  35484  fineqvrep  35508  fineqvpow  35509  axreg  35521  axregscl  35522  axregs  35533  axpowg  35540  onvfowev  35581  lfuhgr3  35593  loop1cycl  35610  satfvsucsuc  35838  satf0op  35850  axextprim  36174  axrepprim  36175  axunprim  36176  axpowprim  36177  axregprim  36178  axinfprim  36179  axacprim  36180  dftr6  36224  coep  36225  coepr  36226  dffr5  36227  cnvco1  36232  cnvco2  36233  eldm3  36234  fundmpss  36240  dfdm5  36246  dfrn5  36247  elima4  36249  axextdfeq  36268  19.12b  36272  axextndbi  36275  brtxp  36351  brpprod  36356  brsset  36360  dfon3  36363  brtxpsd  36365  elfix  36374  dffix2  36376  sscoid  36384  dffun10  36385  elfuns  36386  elsingles  36389  snelsingles  36393  dfiota3  36394  brimg  36408  brapply  36409  brcup  36410  brcap  36411  lemsuccf  36412  funpartlem  36415  brrestrict  36422  dfrecs2  36423  dfrdg4  36424  sumeq2si  36695  prodeq2si  36697  cbvoprab2vw  36731  cbvoprab23vw  36733  cbvprodvw2  36740  neifg  36863  regsfromregtco  37030  regsfromunir1  37032  mh-prprimbi  37035  mh-unprimbi  37036  mh-infprim1bi  37038  mh-infprim2bi  37039  mh-infprim3bi  37040  bj-df-sb  37253  bj-dfsbc  37255  bj-equsexval  37263  bj-eeanvw  37321  bj-substw  37331  eliminable-abelv  37485  eliminable-abelab  37486  bj-denoteslem  37487  bj-rexvw  37496  bj-csbsnlem  37519  bj-gabima  37557  bj-snsetex  37580  bj-elsngl  37585  bj-snglc  37586  bj-abex  37647  bj-clex  37648  bj-clel3gALT  37665  bj-nul  37673  bj-dfid2ALT  37682  bj-rep  37691  bj-axseprep  37692  bj-restpw  37715  bj-restuni  37720  bj-dfmpoa  37741  bj-opabco  37813  bj-xpcossxp  37814  bj-imdirco  37815  mptsnunlem  37965  topdifinffinlem  37974  difunieq  38001  wl-dfclab  38221  poimirlem26  38278  ismblfin  38293  itg2addnclem3  38305  itg2addnc  38306  ismgmOLD  38482  sbcexfi  38747  sbccom2lem  38754  eldmres  38907  ecinn0  38983  ineleq  38984  moantr  39002  dmcnvep  39018  rnxrn  39051  rnxrnres  39052  dmsucmap  39098  dfcoss2  39133  dfcoss3  39134  cosscnv  39136  coss1cnvres  39137  coss2cnvepres  39138  1cossres  39149  cocossss  39156  rncossdmcoss  39175  eldmcoss2  39179  coss0  39199  cossid  39200  dfssr2  39209  eldmqs1cossres  39374  prtlem16  39624  prter2  39636  islshpat  39772  islpln5  40290  islvol5  40334  pmapglb  40525  polval2N  40661  cdlemftr3  41320  dibelval3  41902  dicelval3  41935  dihglb2  42097  sn-axrep5v  42969  prjspeclsp  43327  euabsn2w  43394  diophrex  43489  onsupmaxb  43949  nnoeomeqom  44022  tfsconcatlem  44046  tfsconcat0i  44055  rp-isfinite6  44227  snen1g  44233  relintab  44292  imaiun1  44360  coiun1  44361  clsk3nimkb  44749  expandexn  44982  ismnuprim  44987  rr-groth  44992  ismnushort  44994  rr-grothshortbi  44996  19.36vv  45076  19.37vv  45078  pm11.58  45083  pm11.6  45085  pm13.192  45103  2sbc5g  45109  iotasbc2  45113  onfrALTlem5  45234  onfrALTlem1  45240  ax6e2nd  45250  2sb5nd  45252  en3lplem2VD  45535  onfrALTlem5VD  45576  relopabVD  45592  ax6e2ndVD  45599  2sb5ndVD  45601  ax6e2ndALT  45621  2sb5ndALT  45623  dfac5prim  45682  brpermmodel  45695  permaxrep  45698  permac8prim  45706  rfcnnnub  45739  stoweidlem34  46731  stoweidlem35  46732  stoweidlem60  46757  smfpimcc  47505  ichexmpl1  48201  sprid  48206  dfgric2  48663  usgrgrtrirex  48698  grlimgrtri  48751  eliunxp2  49097  mosssn2  49578  coxp  49594  istermc  50235  setrec1lem3  50450  elpglem3  50474  eximp-surprise  50545  alsbii  50561