Theorem exbii 1847

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

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

This theorem is referenced by:  2exbii  1848  3exbii  1849  exanali  1858  exancom  1860  19.43  1882  19.41vv  1950  19.41vvv  1951  19.41vvvv  1952  exdistr  1954  exdistr2  1958  19.42vvvOLD  1960  3exdistr  1961  19.12vvv  1994  equsexvwOLD  2011  excom13  2170  exrot4  2172  equsexv  2268  2sb5  2281  dfsb7  2284  dfsb7OLD  2285  eeor  2353  19.12vv  2367  eean  2368  eeeanv  2370  ee4anv  2371  2sb8ev  2374  equsexALT  2440  2sb5rf  2495  2sb8e  2575  mo4  2649  eu6lem  2657  eubii  2669  sb8eulem  2683  eu1  2693  sbmo  2697  2moswapv  2713  2moswap  2728  euae  2746  clabel  2962  sbabel  3018  nabbi  3124  rexbii2  3248  rexcom4  3252  2ex2rexrot  3253  rexanidOLD  3256  r2exlem  3305  r19.41v  3350  r19.41  3351  rexcom  3358  isset  3509  rexv  3523  cgsex4g  3542  ceqsex2  3546  ceqsex2v  3547  ceqsex3v  3548  gencbvex  3552  vtocl2OLD  3565  spc3egv  3607  spc3gv  3608  ceqsrexv  3652  rexab  3689  rexrab2  3696  euxfrw  3715  euxfr  3717  euind  3718  reu6  3720  reu3  3721  2reuswap  3740  2reuswap2  3741  reuind  3747  2reu5lem3  3751  2reu5  3752  2rmoswap  3755  sbccomlem  3856  rmo2  3873  rmoanim  3881  rmoanimALT  3882  rexun  4169  reupick3  4291  euelss  4293  ndisj  4330  abn0  4339  pssnel  4423  rexsns  4612  exsnrex  4621  snprc  4656  euabsn2  4664  reusn  4666  eusn  4669  elpreqpr  4800  elunirab  4857  unipr  4858  uniun  4864  uniin  4865  uni0b  4867  uniintsn  4916  iuncom4  4930  dfiun2g  4958  dfiun2gOLD  4959  iunn0  4992  iunxiun  5022  disjor  5049  cbvopab2  5144  cbvopab2v  5147  unopab  5148  axrep1  5194  axrep4  5198  axrep5  5199  axrep6  5200  zfrep4  5203  axsepgfromrep  5204  axnulALT  5211  0ex  5214  vnex  5221  inex1  5224  inuni  5249  axpweq  5268  zfpow  5270  axpow2  5271  axpow3  5272  vpwex  5281  zfpair  5325  zfpair2  5334  eqvinop  5381  copsexgw  5384  copsexg  5385  opabn0  5443  iunopab  5449  dfid3  5465  opeliunxp  5622  xpiundi  5625  xpiundir  5626  elvvv  5630  csbxp  5653  eliunxp  5711  exopxfr  5717  relop  5724  opelco2g  5741  cnvco  5759  cnvuni  5760  dfdm3  5761  dfrn2  5762  dfrn3  5763  elrng  5765  dfdm4  5767  csbdm  5769  eldm2g  5771  dmun  5782  dmin  5783  dmiun  5785  dmuni  5786  dmopab  5787  dmi  5794  dmep  5796  domepOLD  5797  rnep  5800  elrn  5825  rnopab  5829  dmcosseq  5847  dmres  5878  elsnres  5895  dfima2  5934  elima3  5939  imadmrn  5942  imai  5945  args  5960  rniun  6009  xpdifid  6028  ssrnres  6038  dmsnn0  6067  dmsnopg  6073  cnvresima  6090  mptpreima  6095  dfco2  6101  coundi  6103  coundir  6104  resco  6106  imaco  6107  rnco  6108  coiun  6112  coi1  6118  coass  6121  xpco  6143  elsnxp  6145  dffun2  6368  dffun5  6371  imadif  6441  funimaexg  6443  brprcneu  6665  dffv2  6759  fndmin  6818  fvn0ssdmfun  6845  abrexco  7006  imaiun  7007  isomin  7093  dfoprab2  7215  cbvoprab2  7245  zfun  7465  uniex2  7467  uniuni  7487  elxp4  7630  elxp5  7631  fiun  7647  f1iun  7648  f11o  7651  fvresex  7664  opabex3d  7669  opabex3rd  7670  opabex3  7671  abexssex  7674  abexex  7675  oprabrexex2  7682  releldm2  7745  dfopab2  7753  dfoprab3s  7754  fsplit  7815  fsplitOLD  7816  frxp  7823  suppvalbr  7837  cnvimadfsn  7842  brtpos2  7901  wfrfun  7968  dfrecs3  8012  oarec  8191  oeeu  8232  domen  8525  xpsnen  8604  xpcomco  8610  xpassen  8614  inf2  9089  zfinf  9105  axinf2  9106  zfinf2  9108  rankuni  9295  scott0  9318  cp  9323  ween  9464  aceq1  9546  aceq0  9547  aceq2  9548  dfac5lem1  9552  dfac5lem2  9553  dfac5lem3  9554  kmlem3  9581  kmlem14  9592  kmlem15  9593  kmlem16  9594  cflem  9671  cf0  9676  cfval2  9685  cfss  9690  cfslb  9691  fin23lem32  9769  axdc2lem  9873  zfac  9885  ac9  9908  ac9s  9918  axpowndlem3  10024  zfcndrep  10039  zfcndun  10040  zfcndpow  10041  zfcndinf  10043  zfcndac  10044  axgroth5  10249  axgroth2  10250  axgroth6  10253  axgroth3  10256  axgroth4  10257  grothprim  10259  grothtsk  10260  genpass  10434  ltexprlem1  10461  ltexprlem4  10464  supaddc  11611  supadd  11612  supmul1  11613  supmullem2  11615  2rexuz  12303  nnwos  12318  hashgt23el  13788  hashfun  13801  wwlktovfo  14325  xpcogend  14337  cbvsum  15055  cbvprod  15272  iprodmul  15360  maxprmfct  16056  4sqlem12  16295  vdwmc  16317  cshwrepswhash1  16439  imasleval  16817  isacs2  16927  cicsym  17077  gsumval3eu  19027  lidlnz  20004  isbasis2g  21559  tgval2  21567  ntreq0  21688  lmff  21912  cmpfi  22019  is1stc2  22053  1stcelcls  22072  unisngl  22138  isfbas2  22446  elfg  22482  alexsubALTlem3  22660  ustfilxp  22824  metrest  23137  metuel2  23178  restmetu  23183  dchrvmasumlema  26079  istrkg2ld  26249  istrkg3ld  26250  1loopgrvd2  27288  wwlksnextsurj  27681  isgrpo  28277  nmo  30257  reuxfrdf  30258  rexunirn  30259  dmrab  30263  disjorf  30332  fcoinvbr  30361  mpomptxf  30428  cnvoprabOLD  30459  fpwrelmapffslem  30471  ordtconnlem1  31171  ddemeas  31499  omssubaddlem  31561  omssubadd  31562  eulerpartlemgvv  31638  bnj89  31995  bnj133  32001  bnj1019  32055  bnj1101  32060  bnj1109  32062  bnj1143  32066  bnj1198  32071  bnj1304  32095  bnj605  32183  bnj607  32192  bnj600  32195  bnj865  32199  bnj916  32209  bnj983  32227  bnj985v  32229  bnj985  32230  bnj996  32232  bnj1033  32245  bnj1083  32254  bnj1090  32255  bnj1093  32256  bnj1110  32258  bnj1128  32266  bnj1145  32269  bnj1171  32276  bnj1172  32277  bnj1174  32279  bnj1176  32281  bnj1186  32283  bnj1189  32285  bnj1253  32293  bnj1279  32294  bnj1371  32305  bnj1374  32307  bnj1312  32334  exdifsn  32349  lfuhgr3  32370  loop1cycl  32388  satfvsucsuc  32616  satf0op  32628  axextprim  32931  axrepprim  32932  axunprim  32933  axpowprim  32934  axregprim  32935  axinfprim  32936  axacprim  32937  dftr6  32990  coep  32991  coepr  32992  dffr5  32993  dfpo2  32995  cnvco1  32999  cnvco2  33000  eldm3  33001  fundmpss  33013  dfdm5  33020  dfrn5  33021  elima4  33023  axextdfeq  33046  19.12b  33050  axextndbi  33053  brtxp  33345  brpprod  33350  brsset  33354  dfon3  33357  brtxpsd  33359  elfix  33368  dffix2  33370  sscoid  33378  dffun10  33379  elfuns  33380  elsingles  33383  snelsingles  33387  dfiota3  33388  brimg  33402  brapply  33403  brcup  33404  brcap  33405  brsuccf  33406  funpartlem  33407  brrestrict  33414  dfrecs2  33415  dfrdg4  33416  neifg  33723  bj-equsexval  33997  bj-eeanvw  34051  bj-denotes  34192  bj-rexvw  34200  bj-csbsnlem  34224  bj-snsetex  34279  bj-elsngl  34284  bj-snglc  34285  bj-nul  34353  bj-restpw  34387  bj-restuni  34392  bj-dfmpoa  34414  mptsnunlem  34623  topdifinffinlem  34632  difunieq  34659  wl-dfclab  34832  wl-dfrmosb  34857  wl-dfrmov  34858  poimirlem26  34922  ismblfin  34937  itg2addnclem3  34949  itg2addnc  34950  ismgmOLD  35132  sbcexfi  35399  sbccom2lem  35406  eldmres  35534  ecinn0  35611  ineleq  35612  moantr  35620  rnxrn  35650  rnxrnres  35651  dfcoss2  35665  dfcoss3  35666  1cossres  35678  cocossss  35685  rncossdmcoss  35699  eldmcoss2  35703  coss0  35723  cossid  35724  dfssr2  35743  eldmqs1cossres  35897  prtlem16  36009  prter2  36021  islshpat  36157  islpln5  36675  islvol5  36719  pmapglb  36910  polval2N  37046  cdlemftr3  37705  dibelval3  38287  dicelval3  38320  dihglb2  38482  sn-axrep5v  39114  prjspeclsp  39268  diophrex  39378  rp-isfinite6  39890  snen1g  39896  relintab  39949  imaiun1  40002  coiun1  40003  clsk3nimkb  40396  expandexn  40631  ismnuprim  40636  rr-groth  40641  19.36vv  40721  19.37vv  40723  pm11.58  40728  pm11.6  40730  pm13.192  40748  2sbc5g  40754  iotasbc2  40758  onfrALTlem5  40882  onfrALTlem1  40888  ax6e2nd  40898  2sb5nd  40900  en3lplem2VD  41184  onfrALTlem5VD  41225  relopabVD  41241  ax6e2ndVD  41248  2sb5ndVD  41250  ax6e2ndALT  41270  2sb5ndALT  41272  rfcnnnub  41299  inn0f  41341  stoweidlem34  42326  stoweidlem35  42327  stoweidlem60  42352  smfpimcc  43089  ichexmpl1  43638  sprid  43643  opeliun2xp  44388  eliunxp2  44389  setrec1lem3  44799  elpglem3  44822  eximp-surprise  44892