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

Theorem exbii 1763
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 1761 . 2 (∀𝑥(𝜑𝜓) → (∃𝑥𝜑 ↔ ∃𝑥𝜓))
2 exbii.1 . 2 (𝜑𝜓)
31, 2mpg 1714 1 (∃𝑥𝜑 ↔ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  2exbii  1764  3exbii  1765  nfbii  1769  exanali  1772  exancom  1773  19.43  1798  sbequ8  1871  19.12vvv  1893  19.41vv  1901  19.41vvv  1902  19.41vvvv  1903  exdistr  1905  19.42vvv  1907  exdistr2  1908  3exdistr  1909  equsexvw  1918  excom13  2030  exrot4  2032  equsexv  2094  eeor  2156  19.12vv  2167  eean  2168  eeeanv  2170  ee4anv  2171  equsexALT  2281  2sb5  2430  2sb5rf  2438  2sb8e  2454  sb8eu  2490  eu1  2497  sbmo  2502  2moswap  2534  exists1  2548  clabel  2735  sbabel  2778  nabbi  2883  rexbii2  3020  r2exlem  3040  r19.41v  3069  r19.41  3070  isset  3179  rexv  3192  ceqsex2  3216  ceqsex3v  3218  gencbvex  3222  vtocl2  3233  vtocl3  3234  spc3gv  3270  ceqsrexv  3305  rexab  3335  rexrab2  3340  euxfr  3358  euind  3359  reu6  3361  reu3  3362  2reuswap  3376  reuind  3377  2reu5lem3  3381  2reu5  3382  sbccomlem  3474  rmo2  3491  rexun  3754  reupick3  3870  euelss  3872  abn0  3907  pssnel  3990  rexsns  4163  exsnrex  4167  snprc  4196  euabsn2  4203  reusn  4205  eusn  4208  elpreqpr  4329  elunirab  4378  unipr  4379  uniun  4386  uniin  4387  uni0b  4393  uniintsn  4443  iuncom4  4458  dfiun2g  4482  iunn0  4510  iunxiun  4538  disjor  4561  cbvopab2  4650  cbvopab2v  4653  unopab  4654  axrep1  4694  axrep4  4697  axrep5  4698  zfrep4  4701  axsep  4702  zfnuleu  4708  axnulALT  4709  0ex  4712  vprc  4718  inex1  4721  inuni  4747  axpweq  4762  zfpow  4764  axpow2  4765  axpow3  4766  pwex  4768  zfpair  4825  zfpair2  4828  eqvinop  4874  copsexg  4875  opabn0  4920  iunopab  4925  dfid3  4943  elxp2OLD  5046  opeliunxp  5082  xpiundi  5085  xpiundir  5086  elvvv  5090  csbxp  5112  eliunxp  5168  exopxfr  5174  relop  5181  opelco2g  5198  cnvco  5217  cnvuni  5218  dfdm3  5219  dfrn2  5220  dfrn3  5221  elrng  5223  dfdm4  5224  csbdm  5226  eldm2g  5228  dmun  5239  dmin  5240  dmiun  5241  dmuni  5242  dmopab  5243  dmi  5247  elrn  5273  rnopab  5277  dmcosseq  5294  dmres  5325  elres  5341  elsnres  5342  dfima2  5373  elima3  5378  imadmrn  5381  imai  5383  args  5398  rniun  5447  xpdifid  5466  ssrnres  5476  dmsnn0  5503  dmsnopg  5509  cnvresima  5526  mptpreima  5530  dfco2  5536  coundi  5538  coundir  5539  resco  5541  imaco  5542  rnco  5543  coiun  5547  coi1  5553  coass  5556  xpco  5577  elsnxp  5579  elsnxpOLD  5580  dffun2  5799  dffun5  5802  imadif  5872  funimaexg  5874  brprcneu  6080  dffv2  6165  fndmin  6216  fvn0ssdmfun  6242  abrexco  6383  imaiun  6384  isomin  6464  dfoprab2  6576  cbvoprab2  6603  zfun  6825  uniex2  6827  uniuni  6842  elxp4  6980  elxp5  6981  fun11iun  6996  f11o  6998  fvresex  7009  opabex3d  7014  opabex3  7015  abexssex  7018  abexex  7019  oprabrexex2  7026  releldm2  7086  dfopab2  7090  dfoprab3s  7091  fsplit  7146  frxp  7151  suppvalbr  7163  cnvimadfsn  7168  brtpos2  7222  wfrfun  7289  dfrecs3  7333  oarec  7506  oeeu  7547  domen  7831  mapsnen  7897  xpsnen  7906  xpcomco  7912  xpassen  7916  inf2  8380  zfinf  8396  axinf2  8397  zfinf2  8399  rankuni  8586  scott0  8609  cp  8614  ween  8718  aceq1  8800  aceq0  8801  aceq2  8802  dfac5lem1  8806  dfac5lem2  8807  dfac5lem3  8808  kmlem3  8834  kmlem14  8845  kmlem15  8846  kmlem16  8847  cflem  8928  cf0  8933  cfval2  8942  cfss  8947  cfslb  8948  fin23lem32  9026  axdc2lem  9130  zfac  9142  ac9  9165  ac9s  9175  axpowndlem3  9277  zfcndrep  9292  zfcndun  9293  zfcndpow  9294  zfcndinf  9296  zfcndac  9297  axgroth5  9502  axgroth2  9503  grothpw  9504  axgroth6  9506  axgroth3  9509  axgroth4  9510  grothprim  9512  grothtsk  9513  genpass  9687  ltexprlem1  9714  ltexprlem4  9717  supaddc  10839  supadd  10840  supmul1  10841  supmullem2  10843  2rexuz  11574  nnwos  11589  hashfun  13038  wwlktovfo  13497  xpcogend  13509  cbvsum  14221  cbvprod  14432  iprodmul  14521  maxprmfct  15207  4sqlem12  15446  vdwmc  15468  cshwrepswhash1  15595  imasleval  15972  isacs2  16085  cicsym  16235  gsumval3eu  18076  lidlnz  18997  isbasis2g  20510  tgval2  20518  ntreq0  20638  lmff  20862  cmpfi  20968  is1stc2  21002  1stcelcls  21021  unisngl  21087  isfbas2  21396  elfg  21432  alexsubALTlem3  21610  ustfilxp  21773  metrest  22086  metuel2  22127  restmetu  22132  cmetss  22865  dchrvmasumlema  24933  istrkg2ld  25103  istrkg3ld  25104  usgraedg4  25709  3v3e3cycl2  25985  wlknwwlknsur  26033  wlkiswwlksur  26040  wwlkextsur  26052  el2wlkonot  26189  el2spthonot  26190  el2wlkonotot0  26192  frgrawopreglem2  26365  usg2spot2nb  26385  isgrpo  26528  nmo  28502  2reuswap2  28505  rexunirn  28508  iunxsngf  28551  disjorf  28567  fcoinvbr  28592  mpt2mptxf  28653  cnvoprab  28679  fpwrelmapffslem  28688  ordtconlem1  29091  ddemeas  29419  omssubaddlem  29481  omssubadd  29482  eulerpartlemgvv  29558  bnj89  29834  bnj133  29840  bnj1019  29897  bnj1101  29902  bnj1109  29904  bnj1143  29908  bnj1198  29913  bnj1304  29937  bnj605  30024  bnj607  30033  bnj600  30036  bnj865  30040  bnj916  30050  bnj983  30068  bnj985  30070  bnj996  30072  bnj1033  30084  bnj1083  30093  bnj1090  30094  bnj1093  30095  bnj1110  30097  bnj1128  30105  bnj1145  30108  bnj1171  30115  bnj1172  30116  bnj1174  30118  bnj1176  30120  bnj1186  30122  bnj1189  30124  bnj1253  30132  bnj1279  30133  bnj1371  30144  bnj1374  30146  bnj1312  30173  axextprim  30625  axrepprim  30626  axunprim  30627  axpowprim  30628  axregprim  30629  axinfprim  30630  axacprim  30631  dftr6  30686  coep  30687  coepr  30688  dffr5  30689  dfpo2  30691  cnvco1  30696  cnvco2  30697  eldm3  30698  fundmpss  30703  dfdm5  30714  dfrn5  30715  elima4  30717  domep  30735  axextdfeq  30740  19.12b  30744  axextndbi  30747  frrlem5c  30823  nofulllem5  30898  brtxp  30950  brpprod  30955  brsset  30959  dfon3  30962  brtxpsd  30964  elfix  30973  dffix2  30975  sscoid  30983  dffun10  30984  elfuns  30985  elsingles  30988  snelsingles  30992  dfiota3  30993  brimg  31007  brapply  31008  brcup  31009  brcap  31010  brsuccf  31011  funpartlem  31012  brrestrict  31019  dfrecs2  31020  dfrdg4  31021  neifg  31329  bj-equsexval  31620  bj-dfssb2  31622  bj-eeanvw  31684  bj-clabel  31764  bj-axrep1  31769  bj-axrep4  31772  bj-axrep5  31773  bj-axsep  31774  bj-zfpow  31776  bj-denotes  31835  bj-rexvwv  31843  bj-rexcom4  31846  bj-csbsnlem  31873  bj-snsetex  31927  bj-elsngl  31932  bj-snglc  31933  bj-nul  31992  bj-restpw  32009  bj-restuni  32014  bj-dfmpt2a  32035  mptsnunlem  32144  topdifinffinlem  32154  poimirlem26  32388  ismblfin  32403  itg2addnclem3  32416  itg2addnc  32417  ismgmOLD  32602  sbcexfi  32873  sbccom2lem  32882  prtlem16  32955  prter2  32967  islshpat  33105  islpln5  33622  islvol5  33666  pmapglb  33857  polval2N  33993  cdlemftr3  34654  dibelval3  35237  dicelval3  35270  dihglb2  35432  diophrex  36140  rp-isfinite6  36666  relintab  36691  imaiun1  36745  coiun1  36746  ndisj  36866  clsk3nimkb  37141  19.36vv  37387  19.37vv  37389  pm11.58  37395  pm11.6  37397  pm13.192  37416  2sbc5g  37422  iotasbc2  37426  onfrALTlem5  37561  onfrALTlem1  37567  ax6e2nd  37578  2sb5nd  37580  en3lplem2VD  37884  relopabVD  37942  ax6e2ndVD  37949  2sb5ndVD  37951  ax6e2ndALT  37971  2sb5ndALT  37973  rfcnnnub  38001  inn0f  38051  stoweidlem34  38710  stoweidlem35  38711  stoweidlem60  38736  rmoanim  39611  2rmoswap  39616  1loopgrvd2  40699  wlknwwlksnsur  41068  wlkwwlksur  41075  wwlksnextsur  41087  frgrwopreglem2  41463  fusgr2wsp2nb  41479  opeliun2xp  41885  eliunxp2  41886  eximp-surprise  42281
  Copyright terms: Public domain W3C validator