MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exbii Structured version   Visualization version   GIF version

Theorem exbii 1933
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
StepHypRef Expression
1 exbi 1932 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1879 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  2exbii  1934  3exbii  1935  exanali  1946  exancom  1947  19.43  1972  19.41vv  2041  19.41vvv  2042  19.41vvvv  2043  exdistr  2045  19.42vvv  2048  exdistr2  2049  3exdistr  2050  sbequ8  2066  19.12vvv  2087  equsexvw  2102  excom13  2212  exrot4  2214  equsexv  2278  2sb5  2290  eeor  2346  19.12vv  2356  eean  2357  eeeanv  2359  ee4anv  2360  equsexALT  2462  2sb5rf  2614  2sb8e  2630  eu6  2645  sb8eu  2677  eu1  2684  sbmo  2689  2moswap  2722  exists1  2736  clabel  2944  sbabel  2988  nabbi  3091  rexanid  3118  rexbii2  3238  r2exlem  3258  r19.41v  3288  r19.41  3289  isset  3412  rexv  3425  ceqsex2  3449  ceqsex3v  3451  gencbvex  3455  vtocl2  3465  vtocl3  3466  spc3gv  3502  ceqsrexv  3541  rexab  3576  rexrab2  3581  euxfr  3601  euind  3602  reu6  3604  reu3  3605  2reuswap  3619  reuind  3620  2reu5lem3  3624  2reu5  3625  sbccomlem  3715  rmo2  3732  rexun  4003  reupick3  4124  euelss  4126  abn0  4166  pssnel  4246  rexsns  4421  exsnrex  4425  snprc  4455  euabsn2  4462  reusn  4464  eusn  4467  elpreqpr  4600  elunirab  4653  unipr  4654  uniun  4662  uniin  4663  uni0b  4668  uniintsn  4717  iuncom4  4731  dfiun2g  4755  iunn0  4783  iunxiun  4811  disjor  4837  cbvopab2  4929  cbvopab2v  4932  unopab  4933  axrep1  4978  axrep4  4982  axrep5  4983  zfrep4  4986  axsep  4987  zfnuleuOLD  4993  axnulALT  4994  0ex  4997  vnex  5004  inex1  5007  inuni  5031  axpweq  5047  zfpow  5049  axpow2  5050  axpow3  5051  vpwex  5060  zfpair  5107  zfpair2  5110  eqvinop  5157  copsexg  5158  opabn0  5214  iunopab  5220  dfid3  5233  opeliunxp  5384  xpiundi  5387  xpiundir  5388  elvvv  5392  csbxp  5416  eliunxp  5475  exopxfr  5481  relop  5488  opelco2g  5505  cnvco  5523  cnvuni  5524  dfdm3  5525  dfrn2  5526  dfrn3  5527  elrng  5529  dfdm4  5531  csbdm  5533  eldm2g  5535  dmun  5546  dmin  5547  dmiun  5548  dmuni  5549  dmopab  5550  dmi  5555  elrn  5581  rnopab  5585  dmcosseq  5602  dmres  5636  elresOLD  5653  elsnres  5654  elridOLD  5677  dfima2  5692  elima3  5697  imadmrn  5700  imai  5702  args  5717  rniun  5768  xpdifid  5787  ssrnres  5797  dmsnn0  5825  dmsnopg  5832  cnvresima  5851  mptpreima  5856  dfco2  5862  coundi  5864  coundir  5865  resco  5867  imaco  5868  rnco  5869  coiun  5873  coi1  5879  coass  5882  xpco  5903  elsnxp  5905  dffun2  6121  dffun5  6124  imadif  6194  funimaexg  6196  brprcneu  6410  dffv2  6502  fndmin  6556  fvn0ssdmfun  6582  abrexco  6736  imaiun  6737  isomin  6821  dfoprab2  6941  cbvoprab2  6968  zfun  7190  uniex2  7192  uniuni  7211  elxp4  7350  elxp5  7351  fun11iun  7366  f11o  7368  fvresex  7379  opabex3d  7385  opabex3  7386  abexssex  7389  abexex  7391  oprabrexex2  7398  releldm2  7460  dfopab2  7464  dfoprab3s  7465  fsplit  7526  frxp  7531  suppvalbr  7543  cnvimadfsn  7548  brtpos2  7603  wfrfun  7671  dfrecs3  7715  oarec  7889  oeeu  7930  domen  8215  xpsnen  8293  xpcomco  8299  xpassen  8303  inf2  8777  zfinf  8793  axinf2  8794  zfinf2  8796  rankuni  8983  scott0  9006  cp  9011  ween  9151  aceq1  9233  aceq0  9234  aceq2  9235  dfac5lem1  9239  dfac5lem2  9240  dfac5lem3  9241  kmlem3  9269  kmlem14  9280  kmlem15  9281  kmlem16  9282  cflem  9363  cf0  9368  cfval2  9377  cfss  9382  cfslb  9383  fin23lem32  9461  axdc2lem  9565  zfac  9577  ac9  9600  ac9s  9610  axpowndlem3  9716  zfcndrep  9731  zfcndun  9732  zfcndpow  9733  zfcndinf  9735  zfcndac  9736  axgroth5  9941  axgroth2  9942  grothpw  9943  axgroth6  9945  axgroth3  9948  axgroth4  9949  grothprim  9951  grothtsk  9952  genpass  10126  ltexprlem1  10153  ltexprlem4  10156  supaddc  11285  supadd  11286  supmul1  11287  supmullem2  11289  2rexuz  11978  nnwos  11994  hashfun  13461  wwlktovfo  13946  xpcogend  13958  cbvsum  14668  cbvprod  14886  iprodmul  14974  maxprmfct  15658  4sqlem12  15897  vdwmc  15919  cshwrepswhash1  16041  imasleval  16426  isacs2  16538  cicsym  16688  gsumval3eu  18526  lidlnz  19457  isbasis2g  20987  tgval2  20995  ntreq0  21116  lmff  21340  cmpfi  21446  is1stc2  21480  1stcelcls  21499  unisngl  21565  isfbas2  21873  elfg  21909  alexsubALTlem3  22087  ustfilxp  22250  metrest  22563  metuel2  22604  restmetu  22609  cmetss  23347  dchrvmasumlema  25426  istrkg2ld  25596  istrkg3ld  25597  1loopgrvd2  26650  wlknwwlksnsurOLD  27040  wlkwwlksurOLD  27048  wwlksnextsur  27060  isgrpo  27703  nmo  29676  2reuswap2  29677  rexunirn  29680  disjorf  29740  fcoinvbr  29767  mpt2mptxf  29827  cnvoprabOLD  29848  fpwrelmapffslem  29857  ordtconnlem1  30318  ddemeas  30647  omssubaddlem  30709  omssubadd  30710  eulerpartlemgvv  30786  bnj89  31135  bnj133  31141  bnj1019  31195  bnj1101  31200  bnj1109  31202  bnj1143  31206  bnj1198  31211  bnj1304  31235  bnj605  31322  bnj607  31331  bnj600  31334  bnj865  31338  bnj916  31348  bnj983  31366  bnj985  31368  bnj996  31370  bnj1033  31382  bnj1083  31391  bnj1090  31392  bnj1093  31393  bnj1110  31395  bnj1128  31403  bnj1145  31406  bnj1171  31413  bnj1172  31414  bnj1174  31416  bnj1176  31418  bnj1186  31420  bnj1189  31422  bnj1253  31430  bnj1279  31431  bnj1371  31442  bnj1374  31444  bnj1312  31471  axextprim  31922  axrepprim  31923  axunprim  31924  axpowprim  31925  axregprim  31926  axinfprim  31927  axacprim  31928  dftr6  31984  coep  31985  coepr  31986  dffr5  31987  dfpo2  31989  cnvco1  31993  cnvco2  31994  eldm3  31995  fundmpss  32008  dfdm5  32018  dfrn5  32019  elima4  32021  domep  32040  axextdfeq  32045  19.12b  32049  axextndbi  32052  frrlem5c  32129  brtxp  32330  brpprod  32335  brsset  32339  dfon3  32342  brtxpsd  32344  elfix  32353  dffix2  32355  sscoid  32363  dffun10  32364  elfuns  32365  elsingles  32368  snelsingles  32372  dfiota3  32373  brimg  32387  brapply  32388  brcup  32389  brcap  32390  brsuccf  32391  funpartlem  32392  brrestrict  32399  dfrecs2  32400  dfrdg4  32401  neifg  32709  bj-equsexval  32975  bj-dfssb2  32977  bj-eeanvw  33041  bj-clabel  33116  bj-axrep1  33121  bj-axrep4  33124  bj-axrep5  33125  bj-axsep  33126  bj-zfpow  33128  bj-cleljustab  33178  bj-denotes  33184  bj-rexvwv  33193  bj-rexcom4  33196  bj-csbsnlem  33225  bj-snsetex  33280  bj-elsngl  33285  bj-snglc  33286  bj-nul  33347  bj-restpw  33375  bj-restuni  33380  bj-dfmpt2a  33401  mptsnunlem  33521  topdifinffinlem  33530  poimirlem26  33767  ismblfin  33782  itg2addnclem3  33794  itg2addnc  33795  ismgmOLD  33979  sbcexfi  34250  sbccom2lem  34258  eldmres  34372  ecinn0  34450  ineleq  34451  moantr  34459  rnxrn  34488  rnxrnres  34489  dfcoss2  34503  dfcoss3  34504  1cossres  34516  cocossss  34523  rncossdmcoss  34537  eldmcoss2  34541  coss0  34561  cossid  34562  dfssr2  34581  prtlem16  34667  prter2  34679  islshpat  34816  islpln5  35334  islvol5  35378  pmapglb  35569  polval2N  35705  cdlemftr3  36364  dibelval3  36946  dicelval3  36979  dihglb2  37141  diophrex  37859  rp-isfinite6  38382  relintab  38407  imaiun1  38461  coiun1  38462  ndisj  38581  clsk3nimkb  38856  19.36vv  39100  19.37vv  39102  pm11.58  39108  pm11.6  39110  pm13.192  39128  2sbc5g  39134  iotasbc2  39138  onfrALTlem5  39273  onfrALTlem1  39279  ax6e2nd  39290  2sb5nd  39292  en3lplem2VD  39591  onfrALTlem5VD  39633  relopabVD  39649  ax6e2ndVD  39656  2sb5ndVD  39658  ax6e2ndALT  39678  2sb5ndALT  39680  rfcnnnub  39707  inn0f  39753  stoweidlem34  40748  stoweidlem35  40749  stoweidlem60  40774  smfpimcc  41514  rmoanim  41709  2rmoswap  41714  sprid  42310  opeliun2xp  42697  eliunxp2  42698  setrec1lem3  43022  elpglem3  43045  eximp-surprise  43119
  Copyright terms: Public domain W3C validator