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

Theorem exbii 1923
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 1922 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1873 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  2exbii  1924  3exbii  1925  exanali  1935  exancom  1936  19.43  1959  19.41vv  2027  19.41vvv  2028  19.41vvvv  2029  exdistr  2031  19.42vvv  2033  exdistr2  2034  3exdistr  2035  sbequ8  2051  19.12vvv  2072  equsexvw  2087  excom13  2193  exrot4  2195  equsexv  2256  eeor  2316  19.12vv  2325  eean  2326  eeeanv  2328  ee4anv  2329  equsexALT  2438  2sb5  2580  2sb5rf  2588  2sb8e  2604  sb8eu  2641  eu1  2648  sbmo  2653  2moswap  2685  exists1  2699  clabel  2887  sbabel  2931  nabbi  3034  rexbii2  3177  r2exlem  3197  r19.41v  3227  r19.41  3228  isset  3347  rexv  3360  ceqsex2  3384  ceqsex3v  3386  gencbvex  3390  vtocl2  3401  vtocl3  3402  spc3gv  3438  ceqsrexv  3475  rexab  3510  rexrab2  3515  euxfr  3533  euind  3534  reu6  3536  reu3  3537  2reuswap  3551  reuind  3552  2reu5lem3  3556  2reu5  3557  sbccomlem  3649  rmo2  3667  rexun  3936  reupick3  4055  euelss  4057  abn0  4097  pssnel  4183  rexsns  4361  exsnrex  4365  snprc  4397  euabsn2  4404  reusn  4406  eusn  4409  elpreqpr  4547  elunirab  4600  unipr  4601  uniun  4608  uniin  4609  uni0b  4615  uniintsn  4666  iuncom4  4680  dfiun2g  4704  iunn0  4732  iunxiun  4760  disjor  4786  cbvopab2  4876  cbvopab2v  4879  unopab  4880  axrep1  4924  axrep4  4927  axrep5  4928  zfrep4  4931  axsep  4932  zfnuleu  4938  axnulALT  4939  0ex  4942  vprc  4948  inex1  4951  inuni  4975  axpweq  4991  zfpow  4993  axpow2  4994  axpow3  4995  pwex  4997  zfpair  5053  zfpair2  5056  eqvinop  5103  copsexg  5104  opabn0  5156  iunopab  5162  dfid3  5175  elxp2OLD  5290  opeliunxp  5327  xpiundi  5330  xpiundir  5331  elvvv  5335  csbxp  5357  eliunxp  5415  exopxfr  5421  relop  5428  opelco2g  5445  cnvco  5463  cnvuni  5464  dfdm3  5465  dfrn2  5466  dfrn3  5467  elrng  5469  dfdm4  5471  csbdm  5473  eldm2g  5475  dmun  5486  dmin  5487  dmiun  5488  dmuni  5489  dmopab  5490  dmi  5495  elrn  5521  rnopab  5525  dmcosseq  5542  dmres  5577  elres  5593  elsnres  5594  dfima2  5626  elima3  5631  imadmrn  5634  imai  5636  args  5651  rniun  5701  xpdifid  5720  ssrnres  5730  dmsnn0  5758  dmsnopg  5765  cnvresima  5784  mptpreima  5789  dfco2  5795  coundi  5797  coundir  5798  resco  5800  imaco  5801  rnco  5802  coiun  5806  coi1  5812  coass  5815  xpco  5836  elsnxp  5838  elsnxpOLD  5839  dffun2  6059  dffun5  6062  imadif  6134  funimaexg  6136  brprcneu  6345  dffv2  6433  fndmin  6487  fvn0ssdmfun  6513  abrexco  6665  imaiun  6666  isomin  6750  dfoprab2  6866  cbvoprab2  6893  zfun  7115  uniex2  7117  uniuni  7136  elxp4  7275  elxp5  7276  fun11iun  7291  f11o  7293  fvresex  7304  opabex3d  7310  opabex3  7311  abexssex  7314  abexex  7316  oprabrexex2  7323  releldm2  7385  dfopab2  7389  dfoprab3s  7390  fsplit  7450  frxp  7455  suppvalbr  7467  cnvimadfsn  7472  brtpos2  7527  wfrfun  7594  dfrecs3  7638  oarec  7811  oeeu  7852  domen  8134  mapsnen  8200  xpsnen  8209  xpcomco  8215  xpassen  8219  inf2  8693  zfinf  8709  axinf2  8710  zfinf2  8712  rankuni  8899  scott0  8922  cp  8927  ween  9048  aceq1  9130  aceq0  9131  aceq2  9132  dfac5lem1  9136  dfac5lem2  9137  dfac5lem3  9138  kmlem3  9166  kmlem14  9177  kmlem15  9178  kmlem16  9179  cflem  9260  cf0  9265  cfval2  9274  cfss  9279  cfslb  9280  fin23lem32  9358  axdc2lem  9462  zfac  9474  ac9  9497  ac9s  9507  axpowndlem3  9613  zfcndrep  9628  zfcndun  9629  zfcndpow  9630  zfcndinf  9632  zfcndac  9633  axgroth5  9838  axgroth2  9839  grothpw  9840  axgroth6  9842  axgroth3  9845  axgroth4  9846  grothprim  9848  grothtsk  9849  genpass  10023  ltexprlem1  10050  ltexprlem4  10053  supaddc  11182  supadd  11183  supmul1  11184  supmullem2  11186  2rexuz  11933  nnwos  11948  hashfun  13416  wwlktovfo  13902  xpcogend  13914  cbvsum  14624  cbvprod  14844  iprodmul  14933  maxprmfct  15623  4sqlem12  15862  vdwmc  15884  cshwrepswhash1  16011  imasleval  16403  isacs2  16515  cicsym  16665  gsumval3eu  18505  lidlnz  19430  isbasis2g  20954  tgval2  20962  ntreq0  21083  lmff  21307  cmpfi  21413  is1stc2  21447  1stcelcls  21466  unisngl  21532  isfbas2  21840  elfg  21876  alexsubALTlem3  22054  ustfilxp  22217  metrest  22530  metuel2  22571  restmetu  22576  cmetss  23313  dchrvmasumlema  25388  istrkg2ld  25558  istrkg3ld  25559  1loopgrvd2  26609  wlknwwlksnsur  26999  wlkwwlksur  27006  wwlksnextsur  27018  isgrpo  27660  nmo  29634  2reuswap2  29636  rexunirn  29639  disjorf  29699  fcoinvbr  29726  mpt2mptxf  29786  cnvoprabOLD  29807  fpwrelmapffslem  29816  ordtconnlem1  30279  ddemeas  30608  omssubaddlem  30670  omssubadd  30671  eulerpartlemgvv  30747  bnj89  31096  bnj133  31102  bnj1019  31157  bnj1101  31162  bnj1109  31164  bnj1143  31168  bnj1198  31173  bnj1304  31197  bnj605  31284  bnj607  31293  bnj600  31296  bnj865  31300  bnj916  31310  bnj983  31328  bnj985  31330  bnj996  31332  bnj1033  31344  bnj1083  31353  bnj1090  31354  bnj1093  31355  bnj1110  31357  bnj1128  31365  bnj1145  31368  bnj1171  31375  bnj1172  31376  bnj1174  31378  bnj1176  31380  bnj1186  31382  bnj1189  31384  bnj1253  31392  bnj1279  31393  bnj1371  31404  bnj1374  31406  bnj1312  31433  axextprim  31885  axrepprim  31886  axunprim  31887  axpowprim  31888  axregprim  31889  axinfprim  31890  axacprim  31891  dftr6  31947  coep  31948  coepr  31949  dffr5  31950  dfpo2  31952  cnvco1  31956  cnvco2  31957  eldm3  31958  fundmpss  31971  dfdm5  31981  dfrn5  31982  elima4  31984  domep  32003  axextdfeq  32008  19.12b  32012  axextndbi  32015  frrlem5c  32092  brtxp  32293  brpprod  32298  brsset  32302  dfon3  32305  brtxpsd  32307  elfix  32316  dffix2  32318  sscoid  32326  dffun10  32327  elfuns  32328  elsingles  32331  snelsingles  32335  dfiota3  32336  brimg  32350  brapply  32351  brcup  32352  brcap  32353  brsuccf  32354  funpartlem  32355  brrestrict  32362  dfrecs2  32363  dfrdg4  32364  neifg  32672  bj-equsexval  32944  bj-dfssb2  32946  bj-eeanvw  33010  bj-clabel  33089  bj-axrep1  33094  bj-axrep4  33097  bj-axrep5  33098  bj-axsep  33099  bj-zfpow  33101  bj-cleljustab  33153  bj-denotes  33164  bj-rexvwv  33172  bj-rexcom4  33175  bj-csbsnlem  33204  bj-snsetex  33257  bj-elsngl  33262  bj-snglc  33263  bj-nul  33324  bj-restpw  33351  bj-restuni  33356  bj-dfmpt2a  33377  mptsnunlem  33496  topdifinffinlem  33506  poimirlem26  33748  ismblfin  33763  itg2addnclem3  33776  itg2addnc  33777  ismgmOLD  33962  sbcexfi  34233  sbccom2lem  34242  eldmres  34360  ecinn0  34441  ineleq  34442  moantr  34450  rnxrn  34479  rnxrnres  34480  dfcoss2  34494  dfcoss3  34495  1cossres  34507  cocossss  34514  rncossdmcoss  34528  eldmcoss2  34532  coss0  34552  cossid  34553  dfssr2  34572  prtlem16  34658  prter2  34670  islshpat  34807  islpln5  35324  islvol5  35368  pmapglb  35559  polval2N  35695  cdlemftr3  36355  dibelval3  36938  dicelval3  36971  dihglb2  37133  diophrex  37841  rp-isfinite6  38366  relintab  38391  imaiun1  38445  coiun1  38446  ndisj  38565  clsk3nimkb  38840  19.36vv  39084  19.37vv  39086  pm11.58  39092  pm11.6  39094  pm13.192  39113  2sbc5g  39119  iotasbc2  39123  onfrALTlem5  39259  onfrALTlem1  39265  ax6e2nd  39276  2sb5nd  39278  en3lplem2VD  39578  onfrALTlem5VD  39620  relopabVD  39636  ax6e2ndVD  39643  2sb5ndVD  39645  ax6e2ndALT  39665  2sb5ndALT  39667  rfcnnnub  39694  inn0f  39741  stoweidlem34  40754  stoweidlem35  40755  stoweidlem60  40780  smfpimcc  41520  rmoanim  41685  2rmoswap  41690  sprid  42234  opeliun2xp  42621  eliunxp2  42622  setrec1lem3  42946  elpglem3  42969  eximp-surprise  43043
  Copyright terms: Public domain W3C validator