Theorem exbii 1855

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

Syntax hints:   ↔ wb 207  ∃wex 1786

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

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  2exbii  1856  3exbii  1857  exanali  1866  exancom  1868  19.43  1889  19.41vv  1957  19.41vvv  1958  19.41vvvv  1959  exdistr  1961  exdistr2  1965  3exdistr  1967  19.12vvv  2001  excom13  2175  exrot4  2177  2sb5  2289  dfsb7  2290  eeor  2342  19.12vv  2355  eean  2356  eeeanv  2358  ee4anv  2359  ee4anvOLD  2360  2sb8ef  2364  equsexALT  2427  2sb5rf  2480  2sb8e  2538  mo4  2570  eu6lem  2577  sb8eulem  2602  cbvmovw  2606  cbvmow  2607  eu1  2614  sbmo  2618  2moswapv  2633  2moswap  2648  euae  2664  issettru  2818  issetlem  2820  clabel  2885  sbabel  2934  nabbib  3038  rextru  3071  rexbii2  3083  r2exlem  3129  r19.41v  3170  r3ex  3179  r19.41  3244  rexcom4  3267  2ex2rexrot  3275  rexv  3460  ceqsex2  3484  ceqsex2v  3485  ceqsex3v  3486  gencbvex  3490  spc3egv  3548  spc3gv  3549  ceqsrexv  3600  rexrab2  3648  euxfrw  3669  euxfr  3671  euind  3672  reu6  3674  reu3  3675  2reuswap  3694  2reuswap2  3695  reuind  3701  2reu5lem3  3705  2reu5  3706  2rmoswap  3709  sbcimdv  3798  sbcg  3802  sbccomlemOLD  3809  rmo2  3826  rmoanim  3833  rmoanimALT  3834  rexun  4132  reupick3  4265  euelss  4267  ndisj  4305  inn0f  4306  pssnel  4406  rexsns  4610  exsnrex  4619  snprc  4656  euabsn2  4664  reusn  4666  eusn  4669  elpreqpr  4805  elunirab  4860  uniprg  4861  uniun  4868  uniin  4869  uni0b  4871  uniintsn  4922  iuncom4  4937  dfiun2g  4966  iunn0  5003  iunxiun  5033  disjor  5061  cbvopab2  5155  cbvopab2v  5158  unopab  5159  axrep1  5207  axrep4v  5211  axrep4  5212  axrep4OLD  5213  axrep5  5214  axrep6  5215  axrep6OLD  5216  zfrep6  5218  zfrep4  5222  axsepgfromrep  5223  axnulALT  5233  0ex  5236  vnexOLD  5247  inex1  5252  inuni  5285  axpweq  5286  zfpow  5302  axpow2  5303  vpwex  5313  zfpair  5357  zfpair2  5370  prex  5374  elOLD  5385  eqvinop  5434  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  opabn0  5502  iunopab  5508  dfid2  5522  dfid3  5523  opeliunxp  5692  opeliun2xp  5693  xpiundi  5696  xpiundir  5697  elvvv  5701  csbxp  5726  eliunxp  5786  exopxfr  5792  relop  5799  opelco2g  5816  cnvco  5834  cnvuni  5835  dfdm3  5836  dfrn2  5837  dfrn3  5838  elrng  5840  dfdm4  5844  csbdm  5846  eldm2g  5848  dmun  5859  dmin  5860  dmiun  5862  dmuni  5863  dmopab  5864  dmi  5870  dmep  5872  rnep  5876  dmxp  5878  rnopab  5903  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  dmres  5971  elsnres  5980  dfima2  6021  elima3  6026  imadmrn  6029  imai  6033  args  6051  rniun  6105  xpdifid  6126  ssrnres  6136  dmsnn0  6165  dmsnopg  6171  cnvresima  6188  mptpreima  6196  dfco2  6203  coundi  6205  coundir  6206  resco  6208  imaco  6209  rnco  6210  rncoOLD  6211  coiun  6215  coi1  6221  coass  6224  xpco  6247  elsnxp  6249  dfpo2  6254  dffun5  6506  imadif  6576  tz6.12-2  6821  brprcneu  6824  brprcneuALT  6825  dffv2  6929  fndmin  6993  fvn0ssdmfun  7022  abrexco  7195  imaiun  7196  isomin  7288  imaeqsexvOLD  7314  dfoprab2  7421  cbvoprab2  7451  zfun  7686  uniex2  7688  uniuni  7712  elxp4  7869  elxp5  7870  fiun  7892  f1iun  7893  f11o  7896  fvresex  7909  opabex3d  7914  opabex3rd  7915  opabex3  7916  abexssex  7919  abexex  7920  oprabrexex2  7927  releldm2  7992  dfopab2  8001  dfoprab3s  8002  fsplit  8063  frxp  8073  suppvalbr  8111  cnvimadfsn  8119  brtpos2  8179  dfrecs3  8309  oarec  8494  oeeu  8536  domen  8905  xpsnen  8996  xpcomco  9002  xpassen  9006  inf2  9542  zfinf  9558  axinf2  9559  zfinf2  9561  brttrcl2  9633  ttrcltr  9635  ttrclresv  9636  ttrclselem2  9645  rankuni  9785  scott0  9808  cp  9813  ween  9955  aceq1  10037  aceq0  10038  aceq2  10039  dfac5lem1  10043  dfac5lem2  10044  dfac5lem3  10045  kmlem3  10073  kmlem14  10084  kmlem15  10085  kmlem16  10086  cflem  10165  cflemOLD  10166  cf0  10171  cfval2  10180  cfss  10185  cfslb  10186  fin23lem32  10264  axdc2lem  10368  zfac  10380  ac9  10403  ac9s  10413  axpowndlem3  10520  zfcndrep  10535  zfcndun  10536  zfcndpow  10537  zfcndinf  10539  zfcndac  10540  axgroth5  10745  axgroth2  10746  axgroth6  10749  axgroth3  10752  axgroth4  10753  grothprim  10755  grothtsk  10756  genpass  10930  ltexprlem1  10957  ltexprlem4  10960  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  2rexuz  12848  nnwos  12863  hashgt23el  14384  hashfun  14397  wwlktovfo  14918  xpcogend  14934  cbvsum  15655  cbvsumv  15656  cbvprod  15876  cbvprodv  15877  prodeq1i  15879  iprodmul  15966  maxprmfct  16677  4sqlem12  16925  vdwmc  16947  cshwrepswhash1  17071  imasleval  17503  isacs2  17617  cicsym  17769  gsumval3eu  19877  lidlnz  21242  isbasis2g  22938  tgval2  22946  ntreq0  23067  lmff  23291  cmpfi  23398  is1stc2  23432  1stcelcls  23451  unisngl  23517  isfbas2  23825  elfg  23861  alexsubALTlem3  24039  ustfilxp  24203  metrest  24514  metuel2  24555  restmetu  24560  dchrvmasumlema  27488  elold  27876  lrrecfr  27960  leadds1  28006  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  mulsuniflem  28166  addsdilem1  28168  addsdilem2  28169  mulsasslem1  28180  mulsasslem2  28181  elreno2  28512  renegscl  28515  readdscl  28516  remulscl  28519  istrkg2ld  28553  istrkg3ld  28554  1loopgrvd2  29597  wwlksnextsurj  29993  isgrpo  30593  nmo  32584  reuxfrdf  32585  rexunirn  32586  dmrab  32591  disjorf  32675  fcoinvbr  32701  mpomptxf  32777  fpwrelmapffslem  32831  1arithidom  33627  ordtconnlem1  34115  ddemeas  34427  omssubaddlem  34490  omssubadd  34491  eulerpartlemgvv  34567  bnj89  34911  bnj133  34917  bnj1019  34969  bnj1101  34974  bnj1109  34976  bnj1143  34979  bnj1198  34984  bnj1304  35008  bnj605  35096  bnj607  35105  bnj600  35108  bnj865  35112  bnj916  35122  bnj983  35140  bnj985v  35142  bnj985  35143  bnj996  35145  bnj1033  35158  bnj1083  35167  bnj1090  35168  bnj1093  35169  bnj1110  35171  bnj1128  35179  bnj1145  35182  bnj1171  35189  bnj1172  35190  bnj1174  35192  bnj1176  35194  bnj1186  35196  bnj1189  35198  bnj1253  35206  bnj1279  35207  bnj1371  35218  bnj1374  35220  bnj1312  35247  exdifsn  35268  axnulALT2  35271  axprALT2  35297  fineqvrep  35302  fineqvpow  35303  axreg  35315  axregscl  35316  axregs  35327  axpowg  35334  lfuhgr3  35355  loop1cycl  35372  satfvsucsuc  35600  satf0op  35612  axextprim  35936  axrepprim  35937  axunprim  35938  axpowprim  35939  axregprim  35940  axinfprim  35941  axacprim  35942  dftr6  35986  coep  35987  coepr  35988  dffr5  35989  cnvco1  35994  cnvco2  35995  eldm3  35996  fundmpss  36002  dfdm5  36008  dfrn5  36009  elima4  36011  axextdfeq  36030  19.12b  36034  axextndbi  36037  brtxp  36113  brpprod  36118  brsset  36122  dfon3  36125  brtxpsd  36127  elfix  36136  dffix2  36138  sscoid  36146  dffun10  36147  elfuns  36148  elsingles  36151  snelsingles  36155  dfiota3  36156  brimg  36170  brapply  36171  brcup  36172  brcap  36173  lemsuccf  36174  funpartlem  36177  brrestrict  36184  dfrecs2  36185  dfrdg4  36186  sumeq2si  36437  prodeq2si  36439  cbvoprab2vw  36473  cbvoprab23vw  36475  cbvprodvw2  36482  neifg  36606  regsfromregtco  36773  regsfromunir1  36775  mh-prprimbi  36778  mh-unprimbi  36779  mh-infprim1bi  36781  mh-infprim2bi  36782  mh-infprim3bi  36783  bj-df-sb  36997  bj-dfsbc  36999  bj-equsexval  37007  bj-eeanvw  37065  bj-substw  37075  eliminable-abelv  37229  eliminable-abelab  37230  bj-denoteslem  37231  bj-rexvw  37240  bj-csbsnlem  37263  bj-gabima  37300  bj-snsetex  37323  bj-elsngl  37328  bj-snglc  37329  bj-abex  37390  bj-clex  37391  bj-clel3gALT  37408  bj-nul  37416  bj-dfid2ALT  37425  bj-rep  37433  bj-axseprep  37434  bj-restpw  37457  bj-restuni  37462  bj-dfmpoa  37483  bj-opabco  37555  bj-xpcossxp  37556  bj-imdirco  37557  mptsnunlem  37707  topdifinffinlem  37716  difunieq  37743  wl-dfclab  37963  poimirlem26  38020  ismblfin  38035  itg2addnclem3  38047  itg2addnc  38048  ismgmOLD  38224  sbcexfi  38491  sbccom2lem  38498  eldmres  38651  ecinn0  38727  ineleq  38728  moantr  38746  dmcnvep  38762  rnxrn  38795  rnxrnres  38796  dmsucmap  38842  dfcoss2  38877  dfcoss3  38878  cosscnv  38880  coss1cnvres  38881  coss2cnvepres  38882  1cossres  38893  cocossss  38900  rncossdmcoss  38919  eldmcoss2  38923  coss0  38943  cossid  38944  dfssr2  38953  eldmqs1cossres  39118  prtlem16  39368  prter2  39380  islshpat  39516  islpln5  40034  islvol5  40078  pmapglb  40269  polval2N  40405  cdlemftr3  41064  dibelval3  41646  dicelval3  41679  dihglb2  41841  sn-axrep5v  42711  prjspeclsp  43069  euabsn2w  43136  diophrex  43231  onsupmaxb  43691  nnoeomeqom  43764  tfsconcatlem  43788  tfsconcat0i  43797  rp-isfinite6  43969  snen1g  43975  relintab  44034  imaiun1  44102  coiun1  44103  clsk3nimkb  44491  expandexn  44740  ismnuprim  44745  rr-groth  44750  ismnushort  44752  rr-grothshortbi  44754  19.36vv  44834  19.37vv  44836  pm11.58  44841  pm11.6  44843  pm13.192  44861  2sbc5g  44867  iotasbc2  44871  onfrALTlem5  44993  onfrALTlem1  44999  ax6e2nd  45009  2sb5nd  45011  en3lplem2VD  45294  onfrALTlem5VD  45335  relopabVD  45351  ax6e2ndVD  45358  2sb5ndVD  45360  ax6e2ndALT  45380  2sb5ndALT  45382  dfac5prim  45441  brpermmodel  45454  permaxrep  45457  permac8prim  45465  rfcnnnub  45491  stoweidlem34  46484  stoweidlem35  46485  stoweidlem60  46510  smfpimcc  47258  ichexmpl1  47951  sprid  47956  dfgric2  48413  usgrgrtrirex  48448  grlimgrtri  48501  eliunxp2  48832  mosssn2  49314  coxp  49330  istermc  49971  setrec1lem3  50186  elpglem3  50210  eximp-surprise  50281