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 1798	1 ⊢ (∃𝑥𝜑 ↔ ∃𝑥𝜓)

Syntax hints:   ↔ wb 208  ∃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 209  df-ex 1781

This theorem is referenced by:  2exbii  1849  3exbii  1850  exanali  1859  exancom  1861  19.43  1883  19.41vv  1951  19.41vvv  1952  19.41vvvv  1953  exdistr  1955  exdistr2  1959  19.42vvvOLD  1961  3exdistr  1962  19.12vvv  1995  equsexvwOLD  2012  excom13  2171  exrot4  2173  equsexv  2269  2sb5  2282  dfsb7  2285  dfsb7OLD  2286  eeor  2354  19.12vv  2368  eean  2369  eeeanv  2371  ee4anv  2372  2sb8ev  2375  equsexALT  2441  2sb5rf  2496  2sb8e  2576  mo4  2650  eu6lem  2658  eubii  2670  sb8eulem  2684  eu1  2694  sbmo  2698  2moswapv  2714  2moswap  2729  euae  2745  clabel  2959  sbabel  3015  nabbi  3121  rexbii2  3245  rexcom4  3249  2ex2rexrot  3250  rexanidOLD  3253  r2exlem  3302  r19.41v  3347  r19.41  3348  rexcom  3355  isset  3506  rexv  3520  cgsex4g  3539  ceqsex2  3543  ceqsex2v  3544  ceqsex3v  3545  gencbvex  3549  vtocl2OLD  3562  spc3egv  3604  spc3gv  3605  ceqsrexv  3649  rexab  3686  rexrab2  3693  euxfrw  3712  euxfr  3714  euind  3715  reu6  3717  reu3  3718  2reuswap  3737  2reuswap2  3738  reuind  3744  2reu5lem3  3748  2reu5  3749  2rmoswap  3752  sbccomlem  3853  rmo2  3870  rmoanim  3878  rmoanimALT  3879  rexun  4166  reupick3  4288  euelss  4290  ndisj  4327  abn0  4336  pssnel  4420  rexsns  4609  exsnrex  4618  snprc  4653  euabsn2  4661  reusn  4663  eusn  4666  elpreqpr  4797  elunirab  4854  unipr  4855  uniun  4861  uniin  4862  uni0b  4864  uniintsn  4913  iuncom4  4927  dfiun2g  4955  dfiun2gOLD  4956  iunn0  4989  iunxiun  5019  disjor  5046  cbvopab2  5141  cbvopab2v  5144  unopab  5145  axrep1  5191  axrep4  5195  axrep5  5196  axrep6  5197  zfrep4  5200  axsepgfromrep  5201  axnulALT  5208  0ex  5211  vnex  5218  inex1  5221  inuni  5246  axpweq  5265  zfpow  5267  axpow2  5268  axpow3  5269  vpwex  5278  zfpair  5322  zfpair2  5331  eqvinop  5378  copsexgw  5381  copsexg  5382  opabn0  5440  iunopab  5446  dfid3  5462  opeliunxp  5619  xpiundi  5622  xpiundir  5623  elvvv  5627  csbxp  5650  eliunxp  5708  exopxfr  5714  relop  5721  opelco2g  5738  cnvco  5756  cnvuni  5757  dfdm3  5758  dfrn2  5759  dfrn3  5760  elrng  5762  dfdm4  5764  csbdm  5766  eldm2g  5768  dmun  5779  dmin  5780  dmiun  5782  dmuni  5783  dmopab  5784  dmi  5791  dmep  5793  domepOLD  5794  rnep  5797  elrn  5822  rnopab  5826  dmcosseq  5844  dmres  5875  elsnres  5892  dfima2  5931  elima3  5936  imadmrn  5939  imai  5942  args  5957  rniun  6006  xpdifid  6025  ssrnres  6035  dmsnn0  6064  dmsnopg  6070  cnvresima  6087  mptpreima  6092  dfco2  6098  coundi  6100  coundir  6101  resco  6103  imaco  6104  rnco  6105  coiun  6109  coi1  6115  coass  6118  xpco  6140  elsnxp  6142  dffun2  6365  dffun5  6368  imadif  6438  funimaexg  6440  brprcneu  6662  dffv2  6756  fndmin  6815  fvn0ssdmfun  6842  abrexco  7003  imaiun  7004  isomin  7090  dfoprab2  7212  cbvoprab2  7242  zfun  7462  uniex2  7464  uniuni  7484  elxp4  7627  elxp5  7628  fiun  7644  f1iun  7645  f11o  7648  fvresex  7661  opabex3d  7666  opabex3rd  7667  opabex3  7668  abexssex  7671  abexex  7672  oprabrexex2  7679  releldm2  7742  dfopab2  7750  dfoprab3s  7751  fsplit  7812  fsplitOLD  7813  frxp  7820  suppvalbr  7834  cnvimadfsn  7839  brtpos2  7898  wfrfun  7965  dfrecs3  8009  oarec  8188  oeeu  8229  domen  8522  xpsnen  8601  xpcomco  8607  xpassen  8611  inf2  9086  zfinf  9102  axinf2  9103  zfinf2  9105  rankuni  9292  scott0  9315  cp  9320  ween  9461  aceq1  9543  aceq0  9544  aceq2  9545  dfac5lem1  9549  dfac5lem2  9550  dfac5lem3  9551  kmlem3  9578  kmlem14  9589  kmlem15  9590  kmlem16  9591  cflem  9668  cf0  9673  cfval2  9682  cfss  9687  cfslb  9688  fin23lem32  9766  axdc2lem  9870  zfac  9882  ac9  9905  ac9s  9915  axpowndlem3  10021  zfcndrep  10036  zfcndun  10037  zfcndpow  10038  zfcndinf  10040  zfcndac  10041  axgroth5  10246  axgroth2  10247  axgroth6  10250  axgroth3  10253  axgroth4  10254  grothprim  10256  grothtsk  10257  genpass  10431  ltexprlem1  10458  ltexprlem4  10461  supaddc  11608  supadd  11609  supmul1  11610  supmullem2  11612  2rexuz  12301  nnwos  12316  hashgt23el  13786  hashfun  13799  wwlktovfo  14322  xpcogend  14334  cbvsum  15052  cbvprod  15269  iprodmul  15357  maxprmfct  16053  4sqlem12  16292  vdwmc  16314  cshwrepswhash1  16436  imasleval  16814  isacs2  16924  cicsym  17074  gsumval3eu  19024  lidlnz  20001  isbasis2g  21556  tgval2  21564  ntreq0  21685  lmff  21909  cmpfi  22016  is1stc2  22050  1stcelcls  22069  unisngl  22135  isfbas2  22443  elfg  22479  alexsubALTlem3  22657  ustfilxp  22821  metrest  23134  metuel2  23175  restmetu  23180  dchrvmasumlema  26076  istrkg2ld  26246  istrkg3ld  26247  1loopgrvd2  27285  wwlksnextsurj  27678  isgrpo  28274  nmo  30254  reuxfrdf  30255  rexunirn  30256  dmrab  30260  disjorf  30329  fcoinvbr  30358  mpomptxf  30425  cnvoprabOLD  30456  fpwrelmapffslem  30468  ordtconnlem1  31167  ddemeas  31495  omssubaddlem  31557  omssubadd  31558  eulerpartlemgvv  31634  bnj89  31991  bnj133  31997  bnj1019  32051  bnj1101  32056  bnj1109  32058  bnj1143  32062  bnj1198  32067  bnj1304  32091  bnj605  32179  bnj607  32188  bnj600  32191  bnj865  32195  bnj916  32205  bnj983  32223  bnj985v  32225  bnj985  32226  bnj996  32228  bnj1033  32241  bnj1083  32250  bnj1090  32251  bnj1093  32252  bnj1110  32254  bnj1128  32262  bnj1145  32265  bnj1171  32272  bnj1172  32273  bnj1174  32275  bnj1176  32277  bnj1186  32279  bnj1189  32281  bnj1253  32289  bnj1279  32290  bnj1371  32301  bnj1374  32303  bnj1312  32330  exdifsn  32345  lfuhgr3  32366  loop1cycl  32384  satfvsucsuc  32612  satf0op  32624  axextprim  32927  axrepprim  32928  axunprim  32929  axpowprim  32930  axregprim  32931  axinfprim  32932  axacprim  32933  dftr6  32986  coep  32987  coepr  32988  dffr5  32989  dfpo2  32991  cnvco1  32995  cnvco2  32996  eldm3  32997  fundmpss  33009  dfdm5  33016  dfrn5  33017  elima4  33019  axextdfeq  33042  19.12b  33046  axextndbi  33049  brtxp  33341  brpprod  33346  brsset  33350  dfon3  33353  brtxpsd  33355  elfix  33364  dffix2  33366  sscoid  33374  dffun10  33375  elfuns  33376  elsingles  33379  snelsingles  33383  dfiota3  33384  brimg  33398  brapply  33399  brcup  33400  brcap  33401  brsuccf  33402  funpartlem  33403  brrestrict  33410  dfrecs2  33411  dfrdg4  33412  neifg  33719  bj-equsexval  33993  bj-eeanvw  34047  bj-denoteslem  34188  bj-rexvw  34199  bj-csbsnlem  34223  bj-snsetex  34278  bj-elsngl  34283  bj-snglc  34284  bj-nul  34352  bj-restpw  34386  bj-restuni  34391  bj-dfmpoa  34413  mptsnunlem  34622  topdifinffinlem  34631  difunieq  34658  wl-dfclab  34843  wl-dfrmosb  34868  wl-dfrmov  34869  poimirlem26  34933  ismblfin  34948  itg2addnclem3  34960  itg2addnc  34961  ismgmOLD  35143  sbcexfi  35410  sbccom2lem  35417  eldmres  35545  ecinn0  35622  ineleq  35623  moantr  35631  rnxrn  35661  rnxrnres  35662  dfcoss2  35676  dfcoss3  35677  1cossres  35689  cocossss  35696  rncossdmcoss  35710  eldmcoss2  35714  coss0  35734  cossid  35735  dfssr2  35754  eldmqs1cossres  35908  prtlem16  36020  prter2  36032  islshpat  36168  islpln5  36686  islvol5  36730  pmapglb  36921  polval2N  37057  cdlemftr3  37716  dibelval3  38298  dicelval3  38331  dihglb2  38493  sn-axrep5v  39157  prjspeclsp  39311  diophrex  39421  rp-isfinite6  39933  snen1g  39939  relintab  39992  imaiun1  40045  coiun1  40046  clsk3nimkb  40439  expandexn  40674  ismnuprim  40679  rr-groth  40684  19.36vv  40764  19.37vv  40766  pm11.58  40771  pm11.6  40773  pm13.192  40791  2sbc5g  40797  iotasbc2  40801  onfrALTlem5  40925  onfrALTlem1  40931  ax6e2nd  40941  2sb5nd  40943  en3lplem2VD  41227  onfrALTlem5VD  41268  relopabVD  41284  ax6e2ndVD  41291  2sb5ndVD  41293  ax6e2ndALT  41313  2sb5ndALT  41315  rfcnnnub  41342  inn0f  41384  stoweidlem34  42368  stoweidlem35  42369  stoweidlem60  42394  smfpimcc  43131  ichexmpl1  43680  sprid  43685  opeliun2xp  44430  eliunxp2  44431  setrec1lem3  44841  elpglem3  44864  eximp-surprise  44934