Theorem exbii 1848

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

Syntax hints:   ↔ wb 206  ∃wex 1779

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

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

This theorem is referenced by:  2exbii  1849  3exbii  1850  exanali  1859  exancom  1861  19.43  1882  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1954  exdistr2  1958  3exdistr  1960  19.12vvv  1994  excom13  2165  exrot4  2167  2sb5  2278  dfsb7  2279  eeor  2332  19.12vv  2345  eean  2346  eeeanv  2348  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2355  equsexALT  2418  2sb5rf  2471  2sb8e  2529  mo4  2560  eu6lem  2567  eubii  2579  sb8eulem  2592  cbvmovw  2596  cbvmow  2597  eu1  2604  sbmo  2608  2moswapv  2623  2moswap  2638  euae  2654  issettru  2807  issetlem  2809  clabel  2875  sbabel  2925  nabbib  3029  rextru  3061  rexbii2  3073  r2exlem  3123  r19.41v  3168  r3ex  3177  r19.41  3242  rexcom4  3265  rexcomOLD  3268  2ex2rexrot  3275  rexv  3478  cgsex4gOLD  3498  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  gencbvex  3510  spc3egv  3572  spc3gv  3573  ceqsrexv  3624  rexrab2  3674  euxfrw  3695  euxfr  3697  euind  3698  reu6  3700  reu3  3701  2reuswap  3720  2reuswap2  3721  reuind  3727  2reu5lem3  3731  2reu5  3732  2rmoswap  3735  sbcimdv  3825  sbcg  3829  sbccomlemOLD  3836  rmo2  3853  rmoanim  3860  rmoanimALT  3861  rexun  4162  reupick3  4296  euelss  4298  ndisj  4336  inn0f  4337  pssnel  4437  rexsns  4638  exsnrex  4647  snprc  4684  euabsn2  4692  reusn  4694  eusn  4697  elpreqpr  4834  elunirab  4889  uniprg  4890  uniun  4897  uniin  4898  uni0b  4900  uniintsn  4952  iuncom4  4967  dfiun2g  4997  dfiun2gOLD  4998  iunn0  5034  iunxiun  5064  disjor  5092  cbvopab2  5186  cbvopab2v  5189  unopab  5190  axrep1  5238  axrep4v  5242  axrep4  5243  axrep4OLD  5244  axrep5  5245  axrep6  5246  axrep6OLD  5247  zfrep4  5251  axsepgfromrep  5252  axnulALT  5262  0ex  5265  vnex  5272  inex1  5275  inuni  5308  axpweq  5309  zfpow  5324  axpow2  5325  vpwex  5335  zfpair  5379  zfpair2  5391  el  5400  eqvinop  5450  copsexgw  5453  copsexg  5454  opabn0  5516  iunopab  5522  iunopabOLD  5523  dfid2  5538  dfid3  5539  opeliunxp  5708  opeliun2xp  5709  xpiundi  5712  xpiundir  5713  elvvv  5717  csbxp  5741  eliunxp  5804  exopxfr  5810  relop  5817  opelco2g  5834  cnvco  5852  cnvuni  5853  dfdm3  5854  dfrn2  5855  dfrn3  5856  elrng  5858  dfdm4  5862  csbdm  5864  eldm2g  5866  dmun  5877  dmin  5878  dmiun  5880  dmuni  5881  dmopab  5882  dmi  5888  dmep  5890  rnep  5893  dmxp  5895  rnopab  5921  dmcosseq  5943  dmcosseqOLD  5944  dmres  5986  elsnres  5995  dfima2  6036  elima3  6041  imadmrn  6044  imai  6048  args  6066  rniun  6123  xpdifid  6144  ssrnres  6154  dmsnn0  6183  dmsnopg  6189  cnvresima  6206  mptpreima  6214  dfco2  6221  coundi  6223  coundir  6224  resco  6226  imaco  6227  rnco  6228  coiun  6232  coi1  6238  coass  6241  xpco  6265  elsnxp  6267  dfpo2  6272  dffun2OLDOLD  6526  dffun5  6531  imadif  6603  funimaexgOLD  6607  brprcneu  6851  brprcneuALT  6852  dffv2  6959  fndmin  7020  fvn0ssdmfun  7049  abrexco  7221  imaiun  7222  isomin  7315  imaeqsexvOLD  7341  dfoprab2  7450  cbvoprab2  7480  zfun  7715  uniex2  7717  uniuni  7741  elxp4  7901  elxp5  7902  fiun  7924  f1iun  7925  f11o  7928  fvresex  7941  opabex3d  7947  opabex3rd  7948  opabex3  7949  abexssex  7952  abexex  7953  oprabrexex2  7960  releldm2  8025  dfopab2  8034  dfoprab3s  8035  fsplit  8099  frxp  8108  suppvalbr  8146  cnvimadfsn  8154  brtpos2  8214  dfrecs3  8344  oarec  8529  oeeu  8570  domen  8936  xpsnen  9029  xpcomco  9036  xpassen  9040  dif1enOLD  9132  inf2  9583  zfinf  9599  axinf2  9600  zfinf2  9602  brttrcl2  9674  ttrcltr  9676  ttrclresv  9677  ttrclselem2  9686  rankuni  9823  scott0  9846  cp  9851  ween  9995  aceq1  10077  aceq0  10078  aceq2  10079  dfac5lem1  10083  dfac5lem2  10084  dfac5lem3  10085  kmlem3  10113  kmlem14  10124  kmlem15  10125  kmlem16  10126  cflem  10205  cflemOLD  10206  cf0  10211  cfval2  10220  cfss  10225  cfslb  10226  fin23lem32  10304  axdc2lem  10408  zfac  10420  ac9  10443  ac9s  10453  axpowndlem3  10559  zfcndrep  10574  zfcndun  10575  zfcndpow  10576  zfcndinf  10578  zfcndac  10579  axgroth5  10784  axgroth2  10785  axgroth6  10788  axgroth3  10791  axgroth4  10792  grothprim  10794  grothtsk  10795  genpass  10969  ltexprlem1  10996  ltexprlem4  10999  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  2rexuz  12866  nnwos  12881  hashgt23el  14396  hashfun  14409  wwlktovfo  14931  xpcogend  14947  cbvsum  15668  cbvsumv  15669  cbvprod  15886  cbvprodv  15887  prodeq1i  15889  iprodmul  15976  maxprmfct  16686  4sqlem12  16934  vdwmc  16956  cshwrepswhash1  17080  imasleval  17511  isacs2  17621  cicsym  17773  gsumval3eu  19841  lidlnz  21159  isbasis2g  22842  tgval2  22850  ntreq0  22971  lmff  23195  cmpfi  23302  is1stc2  23336  1stcelcls  23355  unisngl  23421  isfbas2  23729  elfg  23765  alexsubALTlem3  23943  ustfilxp  24107  metrest  24419  metuel2  24460  restmetu  24465  dchrvmasumlema  27418  elold  27788  lrrecfr  27857  sleadd1  27903  addsuniflem  27915  addsasslem1  27917  addsasslem2  27918  mulsuniflem  28059  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  renegscl  28356  readdscl  28357  remulscl  28360  istrkg2ld  28394  istrkg3ld  28395  1loopgrvd2  29438  wwlksnextsurj  29837  isgrpo  30433  nmo  32426  reuxfrdf  32427  rexunirn  32428  dmrab  32433  disjorf  32515  fcoinvbr  32541  mpomptxf  32608  fpwrelmapffslem  32662  1arithidom  33515  ordtconnlem1  33921  ddemeas  34233  omssubaddlem  34297  omssubadd  34298  eulerpartlemgvv  34374  bnj89  34718  bnj133  34724  bnj1019  34776  bnj1101  34781  bnj1109  34783  bnj1143  34787  bnj1198  34792  bnj1304  34816  bnj605  34904  bnj607  34913  bnj600  34916  bnj865  34920  bnj916  34930  bnj983  34948  bnj985v  34950  bnj985  34951  bnj996  34953  bnj1033  34966  bnj1083  34975  bnj1090  34976  bnj1093  34977  bnj1110  34979  bnj1128  34987  bnj1145  34990  bnj1171  34997  bnj1172  34998  bnj1174  35000  bnj1176  35002  bnj1186  35004  bnj1189  35006  bnj1253  35014  bnj1279  35015  bnj1371  35026  bnj1374  35028  bnj1312  35055  exdifsn  35076  fineqvrep  35092  fineqvpow  35093  lfuhgr3  35114  loop1cycl  35131  satfvsucsuc  35359  satf0op  35371  axextprim  35695  axrepprim  35696  axunprim  35697  axpowprim  35698  axregprim  35699  axinfprim  35700  axacprim  35701  dftr6  35745  coep  35746  coepr  35747  dffr5  35748  cnvco1  35753  cnvco2  35754  eldm3  35755  fundmpss  35761  dfdm5  35767  dfrn5  35768  elima4  35770  axextdfeq  35792  19.12b  35796  axextndbi  35799  brtxp  35875  brpprod  35880  brsset  35884  dfon3  35887  brtxpsd  35889  elfix  35898  dffix2  35900  sscoid  35908  dffun10  35909  elfuns  35910  elsingles  35913  snelsingles  35917  dfiota3  35918  brimg  35932  brapply  35933  brcup  35934  brcap  35935  brsuccf  35936  funpartlem  35937  brrestrict  35944  dfrecs2  35945  dfrdg4  35946  sumeq2si  36197  prodeq2si  36199  cbvoprab2vw  36233  cbvoprab23vw  36235  cbvprodvw2  36242  neifg  36366  bj-equsexval  36655  bj-eeanvw  36708  bj-substw  36717  eliminable-abelv  36864  eliminable-abelab  36865  bj-denoteslem  36866  bj-rexvw  36875  bj-csbsnlem  36898  bj-gabima  36935  bj-snsetex  36958  bj-elsngl  36963  bj-snglc  36964  bj-abex  37025  bj-clex  37026  bj-clel3gALT  37043  bj-nul  37051  bj-dfid2ALT  37060  bj-restpw  37087  bj-restuni  37092  bj-dfmpoa  37113  bj-opabco  37183  bj-xpcossxp  37184  bj-imdirco  37185  mptsnunlem  37333  topdifinffinlem  37342  difunieq  37369  wl-dfclab  37591  poimirlem26  37647  ismblfin  37662  itg2addnclem3  37674  itg2addnc  37675  ismgmOLD  37851  sbcexfi  38118  sbccom2lem  38125  eldmres  38266  ecinn0  38342  ineleq  38343  moantr  38353  dmcnvep  38368  rnxrn  38391  rnxrnres  38392  dfcoss2  38411  dfcoss3  38412  cosscnv  38414  coss1cnvres  38415  coss2cnvepres  38416  1cossres  38427  cocossss  38434  rncossdmcoss  38453  eldmcoss2  38457  coss0  38477  cossid  38478  dfssr2  38497  eldmqs1cossres  38658  prtlem16  38869  prter2  38881  islshpat  39017  islpln5  39536  islvol5  39580  pmapglb  39771  polval2N  39907  cdlemftr3  40566  dibelval3  41148  dicelval3  41181  dihglb2  41343  sn-axrep5v  42211  prjspeclsp  42607  euabsn2w  42674  diophrex  42770  onsupmaxb  43235  nnoeomeqom  43308  tfsconcatlem  43332  tfsconcat0i  43341  rp-isfinite6  43514  snen1g  43520  relintab  43579  imaiun1  43647  coiun1  43648  clsk3nimkb  44036  expandexn  44285  ismnuprim  44290  rr-groth  44295  ismnushort  44297  rr-grothshortbi  44299  19.36vv  44379  19.37vv  44381  pm11.58  44386  pm11.6  44388  pm13.192  44406  2sbc5g  44412  iotasbc2  44416  onfrALTlem5  44539  onfrALTlem1  44545  ax6e2nd  44555  2sb5nd  44557  en3lplem2VD  44840  onfrALTlem5VD  44881  relopabVD  44897  ax6e2ndVD  44904  2sb5ndVD  44906  ax6e2ndALT  44926  2sb5ndALT  44928  dfac5prim  44987  brpermmodel  45000  permaxrep  45003  permac8prim  45011  rfcnnnub  45037  stoweidlem34  46039  stoweidlem35  46040  stoweidlem60  46065  smfpimcc  46813  ichexmpl1  47474  sprid  47479  dfgric2  47919  usgrgrtrirex  47953  grlimgrtri  47999  eliunxp2  48326  mosssn2  48809  coxp  48825  istermc  49467  setrec1lem3  49682  elpglem3  49706  eximp-surprise  49777