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

Syntax hints:   ↔ wb 209  ∃wex 1787

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

This theorem depends on definitions:  df-bi 210  df-ex 1788

This theorem is referenced by:  2exbii  1856  3exbii  1857  exanali  1867  exancom  1869  19.43  1890  19.41vv  1959  19.41vvv  1960  19.41vvvv  1961  exdistr  1963  exdistr2  1967  3exdistr  1969  19.12vvv  1998  equsexvwOLD  2015  excom13  2170  exrot4  2172  2sb5  2278  dfsb7  2282  eeor  2335  19.12vv  2349  eean  2350  eeeanv  2352  ee4anv  2353  2sb8ev  2356  equsexALT  2418  2sb5rf  2471  2sb8e  2534  mo4  2565  eu6lem  2572  eubii  2584  sb8eulem  2597  cbvmovw  2601  cbvmow  2602  eu1  2611  sbmo  2615  2moswapv  2630  2moswap  2645  euae  2660  elisset  2812  clabel  2875  sbabel  2931  nabbi  3034  rexbii2  3158  rexcom4  3162  2ex2rexrot  3163  r2exlem  3211  r19.41v  3250  r19.41  3251  rexcom  3258  isset  3411  rexv  3423  cgsex4g  3442  cgsex4gOLD  3443  ceqsex2  3448  ceqsex2v  3449  ceqsex3v  3450  gencbvex  3454  spc3egv  3508  spc3gv  3509  ceqsrexv  3553  rexab  3597  rexrab2  3604  euxfrw  3623  euxfr  3625  euind  3626  reu6  3628  reu3  3629  2reuswap  3648  2reuswap2  3649  reuind  3655  2reu5lem3  3659  2reu5  3660  2rmoswap  3663  sbcimdv  3756  sbcg  3761  sbccomlem  3769  rmo2  3786  rmoanim  3793  rmoanimALT  3794  rexun  4090  reupick3  4220  euelss  4222  ndisj  4268  abn0OLD  4282  pssnel  4371  rexsns  4571  exsnrex  4582  snprc  4619  euabsn2  4627  reusn  4629  eusn  4632  elpreqpr  4763  elunirab  4821  uniprg  4822  uniprOLD  4824  uniun  4830  uniin  4831  uni0b  4833  uniintsn  4884  iuncom4  4898  dfiun2g  4926  iunn0  4961  iunxiun  4991  disjor  5019  cbvopab2  5115  cbvopab2v  5118  unopab  5119  axrep1  5165  axrep4  5169  axrep5  5170  axrep6  5171  zfrep4  5174  axsepgfromrep  5175  axnulALT  5182  0ex  5185  vnex  5192  inex1  5195  inuni  5221  axpweq  5242  zfpow  5244  axpow2  5245  axpow3  5246  vpwex  5255  zfpair  5299  zfpair2  5308  eqvinop  5355  copsexgw  5358  copsexg  5359  opabn0  5419  iunopab  5425  dfid3  5442  opeliunxp  5601  xpiundi  5604  xpiundir  5605  elvvv  5609  csbxp  5632  eliunxp  5691  exopxfr  5697  relop  5704  opelco2g  5721  cnvco  5739  cnvuni  5740  dfdm3  5741  dfrn2  5742  dfrn3  5743  elrng  5745  dfdm4  5749  csbdm  5751  eldm2g  5753  dmun  5764  dmin  5765  dmiun  5767  dmuni  5768  dmopab  5769  dmi  5775  dmep  5777  domepOLD  5778  rnep  5781  rnopab  5808  dmcosseq  5827  dmres  5858  elsnres  5876  dfima2  5916  elima3  5921  imadmrn  5924  imai  5927  args  5942  rniun  5991  xpdifid  6011  ssrnres  6021  dmsnn0  6050  dmsnopg  6056  cnvresima  6073  mptpreima  6081  dfco2  6089  coundi  6091  coundir  6092  resco  6094  imaco  6095  rnco  6096  coiun  6100  coi1  6106  coass  6109  xpco  6132  elsnxp  6134  dffun2  6368  dffun5  6371  imadif  6442  funimaexg  6444  brprcneu  6686  fvprc  6687  dffv2  6784  fndmin  6843  fvn0ssdmfun  6873  abrexco  7035  imaiun  7036  isomin  7124  dfoprab2  7247  cbvoprab2  7277  zfun  7502  uniex2  7504  uniuni  7525  elxp4  7678  elxp5  7679  fiun  7694  f1iun  7695  f11o  7698  fvresex  7711  opabex3d  7716  opabex3rd  7717  opabex3  7718  abexssex  7721  abexex  7722  oprabrexex2  7729  releldm2  7792  dfopab2  7800  dfoprab3s  7801  fsplit  7863  fsplitOLD  7864  frxp  7871  suppvalbr  7885  cnvimadfsn  7892  brtpos2  7952  wfrfun  8043  dfrecs3  8087  oarec  8268  oeeu  8309  domen  8619  xpsnen  8707  xpcomco  8713  xpassen  8717  dif1en  8818  inf2  9216  zfinf  9232  axinf2  9233  zfinf2  9235  rankuni  9444  scott0  9467  cp  9472  ween  9614  aceq1  9696  aceq0  9697  aceq2  9698  dfac5lem1  9702  dfac5lem2  9703  dfac5lem3  9704  kmlem3  9731  kmlem14  9742  kmlem15  9743  kmlem16  9744  cflem  9825  cf0  9830  cfval2  9839  cfss  9844  cfslb  9845  fin23lem32  9923  axdc2lem  10027  zfac  10039  ac9  10062  ac9s  10072  axpowndlem3  10178  zfcndrep  10193  zfcndun  10194  zfcndpow  10195  zfcndinf  10197  zfcndac  10198  axgroth5  10403  axgroth2  10404  axgroth6  10407  axgroth3  10410  axgroth4  10411  grothprim  10413  grothtsk  10414  genpass  10588  ltexprlem1  10615  ltexprlem4  10618  supaddc  11764  supadd  11765  supmul1  11766  supmullem2  11768  2rexuz  12461  nnwos  12476  hashgt23el  13956  hashfun  13969  wwlktovfo  14490  xpcogend  14502  cbvsum  15224  cbvprod  15440  iprodmul  15528  maxprmfct  16229  4sqlem12  16472  vdwmc  16494  cshwrepswhash1  16619  imasleval  17000  isacs2  17110  cicsym  17263  gsumval3eu  19243  lidlnz  20220  isbasis2g  21799  tgval2  21807  ntreq0  21928  lmff  22152  cmpfi  22259  is1stc2  22293  1stcelcls  22312  unisngl  22378  isfbas2  22686  elfg  22722  alexsubALTlem3  22900  ustfilxp  23064  metrest  23376  metuel2  23417  restmetu  23422  dchrvmasumlema  26335  istrkg2ld  26505  istrkg3ld  26506  1loopgrvd2  27545  wwlksnextsurj  27938  isgrpo  28532  nmo  30511  reuxfrdf  30512  rexunirn  30513  dmrab  30517  disjorf  30591  fcoinvbr  30620  mpomptxf  30690  cnvoprabOLD  30729  fpwrelmapffslem  30741  ordtconnlem1  31542  ddemeas  31870  omssubaddlem  31932  omssubadd  31933  eulerpartlemgvv  32009  bnj89  32366  bnj133  32372  bnj1019  32426  bnj1101  32431  bnj1109  32433  bnj1143  32437  bnj1198  32442  bnj1304  32466  bnj605  32554  bnj607  32563  bnj600  32566  bnj865  32570  bnj916  32580  bnj983  32598  bnj985v  32600  bnj985  32601  bnj996  32603  bnj1033  32616  bnj1083  32625  bnj1090  32626  bnj1093  32627  bnj1110  32629  bnj1128  32637  bnj1145  32640  bnj1171  32647  bnj1172  32648  bnj1174  32650  bnj1176  32652  bnj1186  32654  bnj1189  32656  bnj1253  32664  bnj1279  32665  bnj1371  32676  bnj1374  32678  bnj1312  32705  exdifsn  32720  fineqvrep  32731  fineqvpow  32732  lfuhgr3  32748  loop1cycl  32766  satfvsucsuc  32994  satf0op  33006  axextprim  33309  axrepprim  33310  axunprim  33311  axpowprim  33312  axregprim  33313  axinfprim  33314  axacprim  33315  imaeqsexv  33360  dftr6  33387  coep  33388  coepr  33389  dffr5  33390  dfpo2  33392  cnvco1  33396  cnvco2  33397  eldm3  33398  fundmpss  33410  dfdm5  33417  dfrn5  33418  elima4  33420  axextdfeq  33443  19.12b  33447  axextndbi  33450  elold  33739  lrrecfr  33786  brtxp  33868  brpprod  33873  brsset  33877  dfon3  33880  brtxpsd  33882  elfix  33891  dffix2  33893  sscoid  33901  dffun10  33902  elfuns  33903  elsingles  33906  snelsingles  33910  dfiota3  33911  brimg  33925  brapply  33926  brcup  33927  brcap  33928  brsuccf  33929  funpartlem  33930  brrestrict  33937  dfrecs2  33938  dfrdg4  33939  neifg  34246  bj-equsexval  34527  bj-eeanvw  34581  bj-substw  34590  eliminable-abelv  34739  eliminable-abelab  34740  bj-denoteslem  34741  bj-rexvw  34752  bj-csbsnlem  34775  bj-gabima  34814  bj-snsetex  34839  bj-elsngl  34844  bj-snglc  34845  bj-clel3gALT  34907  bj-nul  34913  bj-restpw  34947  bj-restuni  34952  bj-dfmpoa  34973  bj-opabco  35043  bj-xpcossxp  35044  bj-imdirco  35045  mptsnunlem  35195  topdifinffinlem  35204  difunieq  35231  wl-dfclab  35433  poimirlem26  35489  ismblfin  35504  itg2addnclem3  35516  itg2addnc  35517  ismgmOLD  35694  sbcexfi  35961  sbccom2lem  35968  eldmres  36094  ecinn0  36171  ineleq  36172  moantr  36180  rnxrn  36210  rnxrnres  36211  dfcoss2  36225  dfcoss3  36226  1cossres  36238  cocossss  36245  rncossdmcoss  36259  eldmcoss2  36263  coss0  36283  cossid  36284  dfssr2  36303  eldmqs1cossres  36457  prtlem16  36569  prter2  36581  islshpat  36717  islpln5  37235  islvol5  37279  pmapglb  37470  polval2N  37606  cdlemftr3  38265  dibelval3  38847  dicelval3  38880  dihglb2  39042  sn-axrep5v  39848  prjspeclsp  40100  diophrex  40241  rp-isfinite6  40751  snen1g  40757  relintab  40808  imaiun1  40877  coiun1  40878  clsk3nimkb  41268  expandexn  41521  ismnuprim  41526  rr-groth  41531  ismnushort  41533  rr-grothshortbi  41535  19.36vv  41615  19.37vv  41617  pm11.58  41622  pm11.6  41624  pm13.192  41642  2sbc5g  41648  iotasbc2  41652  onfrALTlem5  41776  onfrALTlem1  41782  ax6e2nd  41792  2sb5nd  41794  en3lplem2VD  42078  onfrALTlem5VD  42119  relopabVD  42135  ax6e2ndVD  42142  2sb5ndVD  42144  ax6e2ndALT  42164  2sb5ndALT  42166  rfcnnnub  42193  inn0f  42235  stoweidlem34  43193  stoweidlem35  43194  stoweidlem60  43219  smfpimcc  43956  ichexmpl1  44537  sprid  44542  opeliun2xp  45284  eliunxp2  45285  rextru  45765  mosssn2  45778  setrec1lem3  46009  elpglem3  46032  eximp-surprise  46102