Theorem exbii 1849

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

Syntax hints:   ↔ wb 206  ∃wex 1780

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

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  2exbii  1850  3exbii  1851  exanali  1860  exancom  1862  19.43  1883  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistr  1955  exdistr2  1959  3exdistr  1961  19.12vvv  1995  excom13  2167  exrot4  2169  2sb5  2280  dfsb7  2281  eeor  2334  19.12vv  2347  eean  2348  eeeanv  2350  ee4anv  2351  ee4anvOLD  2352  2sb8ef  2356  equsexALT  2419  2sb5rf  2472  2sb8e  2530  mo4  2561  eu6lem  2568  eubii  2580  sb8eulem  2593  cbvmovw  2597  cbvmow  2598  eu1  2605  sbmo  2609  2moswapv  2624  2moswap  2639  euae  2655  issettru  2809  issetlem  2811  clabel  2877  sbabel  2927  nabbib  3031  rextru  3063  rexbii2  3075  r2exlem  3121  r19.41v  3162  r3ex  3171  r19.41  3236  rexcom4  3259  2ex2rexrot  3267  rexv  3464  cgsex4gOLD  3484  ceqsex2  3490  ceqsex2v  3491  ceqsex3v  3492  gencbvex  3496  spc3egv  3558  spc3gv  3559  ceqsrexv  3610  rexrab2  3659  euxfrw  3680  euxfr  3682  euind  3683  reu6  3685  reu3  3686  2reuswap  3705  2reuswap2  3706  reuind  3712  2reu5lem3  3716  2reu5  3717  2rmoswap  3720  sbcimdv  3810  sbcg  3814  sbccomlemOLD  3821  rmo2  3838  rmoanim  3845  rmoanimALT  3846  rexun  4146  reupick3  4280  euelss  4282  ndisj  4320  inn0f  4321  pssnel  4421  rexsns  4624  exsnrex  4633  snprc  4670  euabsn2  4678  reusn  4680  eusn  4683  elpreqpr  4819  elunirab  4874  uniprg  4875  uniun  4882  uniin  4883  uni0b  4885  uniintsn  4935  iuncom4  4950  dfiun2g  4980  iunn0  5015  iunxiun  5045  disjor  5073  cbvopab2  5167  cbvopab2v  5170  unopab  5171  axrep1  5218  axrep4v  5222  axrep4  5223  axrep4OLD  5224  axrep5  5225  axrep6  5226  axrep6OLD  5227  zfrep4  5231  axsepgfromrep  5232  axnulALT  5242  0ex  5245  vnex  5252  inex1  5255  inuni  5288  axpweq  5289  zfpow  5304  axpow2  5305  vpwex  5315  zfpair  5359  zfpair2  5371  el  5380  eqvinop  5427  copsexgw  5430  copsexg  5431  opabn0  5493  iunopab  5499  dfid2  5513  dfid3  5514  opeliunxp  5683  opeliun2xp  5684  xpiundi  5687  xpiundir  5688  elvvv  5692  csbxp  5716  eliunxp  5777  exopxfr  5783  relop  5790  opelco2g  5807  cnvco  5825  cnvuni  5826  dfdm3  5827  dfrn2  5828  dfrn3  5829  elrng  5831  dfdm4  5835  csbdm  5837  eldm2g  5839  dmun  5850  dmin  5851  dmiun  5853  dmuni  5854  dmopab  5855  dmi  5861  dmep  5863  rnep  5867  dmxp  5869  rnopab  5894  dmcosseq  5917  dmcosseqOLD  5918  dmcosseqOLDOLD  5919  dmres  5961  elsnres  5970  dfima2  6011  elima3  6016  imadmrn  6019  imai  6023  args  6041  rniun  6094  xpdifid  6115  ssrnres  6125  dmsnn0  6154  dmsnopg  6160  cnvresima  6177  mptpreima  6185  dfco2  6192  coundi  6194  coundir  6195  resco  6197  imaco  6198  rnco  6199  rncoOLD  6200  coiun  6204  coi1  6210  coass  6213  xpco  6236  elsnxp  6238  dfpo2  6243  dffun5  6495  imadif  6565  tz6.12-2  6809  brprcneu  6812  brprcneuALT  6813  dffv2  6917  fndmin  6978  fvn0ssdmfun  7007  abrexco  7178  imaiun  7179  isomin  7271  imaeqsexvOLD  7297  dfoprab2  7404  cbvoprab2  7434  zfun  7669  uniex2  7671  uniuni  7695  elxp4  7852  elxp5  7853  fiun  7875  f1iun  7876  f11o  7879  fvresex  7892  opabex3d  7897  opabex3rd  7898  opabex3  7899  abexssex  7902  abexex  7903  oprabrexex2  7910  releldm2  7975  dfopab2  7984  dfoprab3s  7985  fsplit  8047  frxp  8056  suppvalbr  8094  cnvimadfsn  8102  brtpos2  8162  dfrecs3  8292  oarec  8477  oeeu  8518  domen  8884  xpsnen  8974  xpcomco  8980  xpassen  8984  inf2  9513  zfinf  9529  axinf2  9530  zfinf2  9532  brttrcl2  9604  ttrcltr  9606  ttrclresv  9607  ttrclselem2  9616  rankuni  9756  scott0  9779  cp  9784  ween  9926  aceq1  10008  aceq0  10009  aceq2  10010  dfac5lem1  10014  dfac5lem2  10015  dfac5lem3  10016  kmlem3  10044  kmlem14  10055  kmlem15  10056  kmlem16  10057  cflem  10136  cflemOLD  10137  cf0  10142  cfval2  10151  cfss  10156  cfslb  10157  fin23lem32  10235  axdc2lem  10339  zfac  10351  ac9  10374  ac9s  10384  axpowndlem3  10490  zfcndrep  10505  zfcndun  10506  zfcndpow  10507  zfcndinf  10509  zfcndac  10510  axgroth5  10715  axgroth2  10716  axgroth6  10719  axgroth3  10722  axgroth4  10723  grothprim  10725  grothtsk  10726  genpass  10900  ltexprlem1  10927  ltexprlem4  10930  supaddc  12089  supadd  12090  supmul1  12091  supmullem2  12093  2rexuz  12798  nnwos  12813  hashgt23el  14331  hashfun  14344  wwlktovfo  14865  xpcogend  14881  cbvsum  15602  cbvsumv  15603  cbvprod  15820  cbvprodv  15821  prodeq1i  15823  iprodmul  15910  maxprmfct  16620  4sqlem12  16868  vdwmc  16890  cshwrepswhash1  17014  imasleval  17445  isacs2  17559  cicsym  17711  gsumval3eu  19817  lidlnz  21180  isbasis2g  22864  tgval2  22872  ntreq0  22993  lmff  23217  cmpfi  23324  is1stc2  23358  1stcelcls  23377  unisngl  23443  isfbas2  23751  elfg  23787  alexsubALTlem3  23965  ustfilxp  24129  metrest  24440  metuel2  24481  restmetu  24486  dchrvmasumlema  27439  elold  27815  lrrecfr  27887  sleadd1  27933  addsuniflem  27945  addsasslem1  27947  addsasslem2  27948  mulsuniflem  28089  addsdilem1  28091  addsdilem2  28092  mulsasslem1  28103  mulsasslem2  28104  renegscl  28401  readdscl  28402  remulscl  28405  istrkg2ld  28439  istrkg3ld  28440  1loopgrvd2  29483  wwlksnextsurj  29879  isgrpo  30475  nmo  32467  reuxfrdf  32468  rexunirn  32469  dmrab  32474  disjorf  32557  fcoinvbr  32583  mpomptxf  32657  fpwrelmapffslem  32713  1arithidom  33500  ordtconnlem1  33935  ddemeas  34247  omssubaddlem  34310  omssubadd  34311  eulerpartlemgvv  34387  bnj89  34731  bnj133  34737  bnj1019  34789  bnj1101  34794  bnj1109  34796  bnj1143  34800  bnj1198  34805  bnj1304  34829  bnj605  34917  bnj607  34926  bnj600  34929  bnj865  34933  bnj916  34943  bnj983  34961  bnj985v  34963  bnj985  34964  bnj996  34966  bnj1033  34979  bnj1083  34988  bnj1090  34989  bnj1093  34990  bnj1110  34992  bnj1128  35000  bnj1145  35003  bnj1171  35010  bnj1172  35011  bnj1174  35013  bnj1176  35015  bnj1186  35017  bnj1189  35019  bnj1253  35027  bnj1279  35028  bnj1371  35039  bnj1374  35041  bnj1312  35068  exdifsn  35089  axreg  35123  axregscl  35124  fineqvrep  35135  fineqvpow  35136  axregs  35143  lfuhgr3  35162  loop1cycl  35179  satfvsucsuc  35407  satf0op  35419  axextprim  35743  axrepprim  35744  axunprim  35745  axpowprim  35746  axregprim  35747  axinfprim  35748  axacprim  35749  dftr6  35793  coep  35794  coepr  35795  dffr5  35796  cnvco1  35801  cnvco2  35802  eldm3  35803  fundmpss  35809  dfdm5  35815  dfrn5  35816  elima4  35818  axextdfeq  35837  19.12b  35841  axextndbi  35844  brtxp  35920  brpprod  35925  brsset  35929  dfon3  35932  brtxpsd  35934  elfix  35943  dffix2  35945  sscoid  35953  dffun10  35954  elfuns  35955  elsingles  35958  snelsingles  35962  dfiota3  35963  brimg  35977  brapply  35978  brcup  35979  brcap  35980  brsuccf  35981  funpartlem  35982  brrestrict  35989  dfrecs2  35990  dfrdg4  35991  sumeq2si  36242  prodeq2si  36244  cbvoprab2vw  36278  cbvoprab23vw  36280  cbvprodvw2  36287  neifg  36411  bj-equsexval  36700  bj-eeanvw  36753  bj-substw  36762  eliminable-abelv  36909  eliminable-abelab  36910  bj-denoteslem  36911  bj-rexvw  36920  bj-csbsnlem  36943  bj-gabima  36980  bj-snsetex  37003  bj-elsngl  37008  bj-snglc  37009  bj-abex  37070  bj-clex  37071  bj-clel3gALT  37088  bj-nul  37096  bj-dfid2ALT  37105  bj-restpw  37132  bj-restuni  37137  bj-dfmpoa  37158  bj-opabco  37228  bj-xpcossxp  37229  bj-imdirco  37230  mptsnunlem  37378  topdifinffinlem  37387  difunieq  37414  wl-dfclab  37636  poimirlem26  37692  ismblfin  37707  itg2addnclem3  37719  itg2addnc  37720  ismgmOLD  37896  sbcexfi  38163  sbccom2lem  38170  eldmres  38311  ecinn0  38387  ineleq  38388  moantr  38398  dmcnvep  38413  rnxrn  38436  rnxrnres  38437  dfcoss2  38456  dfcoss3  38457  cosscnv  38459  coss1cnvres  38460  coss2cnvepres  38461  1cossres  38472  cocossss  38479  rncossdmcoss  38498  eldmcoss2  38502  coss0  38522  cossid  38523  dfssr2  38542  eldmqs1cossres  38703  prtlem16  38914  prter2  38926  islshpat  39062  islpln5  39580  islvol5  39624  pmapglb  39815  polval2N  39951  cdlemftr3  40610  dibelval3  41192  dicelval3  41225  dihglb2  41387  sn-axrep5v  42255  prjspeclsp  42651  euabsn2w  42718  diophrex  42814  onsupmaxb  43278  nnoeomeqom  43351  tfsconcatlem  43375  tfsconcat0i  43384  rp-isfinite6  43557  snen1g  43563  relintab  43622  imaiun1  43690  coiun1  43691  clsk3nimkb  44079  expandexn  44328  ismnuprim  44333  rr-groth  44338  ismnushort  44340  rr-grothshortbi  44342  19.36vv  44422  19.37vv  44424  pm11.58  44429  pm11.6  44431  pm13.192  44449  2sbc5g  44455  iotasbc2  44459  onfrALTlem5  44581  onfrALTlem1  44587  ax6e2nd  44597  2sb5nd  44599  en3lplem2VD  44882  onfrALTlem5VD  44923  relopabVD  44939  ax6e2ndVD  44946  2sb5ndVD  44948  ax6e2ndALT  44968  2sb5ndALT  44970  dfac5prim  45029  brpermmodel  45042  permaxrep  45045  permac8prim  45053  rfcnnnub  45079  stoweidlem34  46078  stoweidlem35  46079  stoweidlem60  46104  smfpimcc  46852  ichexmpl1  47506  sprid  47511  dfgric2  47952  usgrgrtrirex  47987  grlimgrtri  48040  eliunxp2  48371  mosssn2  48854  coxp  48870  istermc  49512  setrec1lem3  49727  elpglem3  49751  eximp-surprise  49822